1		package(load_event_b_project([event_b_model(none,conc_4,[sees(none,[conc_ctx_0]),refines(none,conc_3),variables(none,[identifier(none,adr_r),identifier(none,adr_w),identifier(none,data),identifier(none,indx_r),identifier(none,indx_w),identifier(none,latest),identifier(none,max_r),identifier(none,max_w),identifier(none,pair_w),identifier(none,reading),identifier(none,slot),identifier(none,x),identifier(none,y)]),invariant(none,[member(rodinpos(conc_4,inv1,internal_inv1I),identifier(none,x),identifier(none,'D')),member(rodinpos(conc_4,inv2,internal_inv2I),identifier(none,data),total_function(none,set_extension(none,[integer(none,0),integer(none,1)]),total_function(none,set_extension(none,[integer(none,0),integer(none,1)]),identifier(none,'D')))),member(rodinpos(conc_4,inv3,internal_inv3I),identifier(none,indx_w),set_extension(none,[integer(none,0),integer(none,1)])),implication(rodinpos(conc_4,inv4,internal_inv4I),member(none,identifier(none,adr_w),set_extension(none,[integer(none,1),integer(none,4),integer(none,5)])),equal(none,identifier(none,'Data'),identifier(none,data))),implication(rodinpos(conc_4,inv5,internal_inv5I),member(none,identifier(none,adr_w),set_extension(none,[integer(none,2),integer(none,3)])),equal(none,identifier(none,'Data'),overwrite(none,identifier(none,data),set_extension(none,[couple(none,[identifier(none,pair_w),overwrite(none,function(none,identifier(none,data),[identifier(none,pair_w)]),set_extension(none,[couple(none,[identifier(none,indx_wp),identifier(none,x)])]))])])))),implication(rodinpos(conc_4,inv6,internal_inv6I),member(none,identifier(none,adr_w),set_extension(none,[integer(none,1),integer(none,3),integer(none,4),integer(none,5)])),equal(none,identifier(none,indx_w),identifier(none,indx_wp))),implication(rodinpos(conc_4,inv7,internal_inv7I),conjunct(none,equal(none,identifier(none,adr_w),integer(none,3)),conjunct(none,equal(none,identifier(none,adr_r),integer(none,3)),equal(none,identifier(none,pair_w),identifier(none,reading)))),negation(none,equal(none,identifier(none,indx_r),identifier(none,indx_wp)))),implication(rodinpos(conc_4,inv8,internal_inv8I),conjunct(none,equal(none,identifier(none,adr_w),integer(none,2)),conjunct(none,equal(none,identifier(none,adr_r),integer(none,3)),equal(none,identifier(none,pair_w),identifier(none,reading)))),negation(none,equal(none,identifier(none,indx_r),identifier(none,indx_wp)))),member(rodinpos(conc_4,inv9,'_xmoPwEDrEeWuxbRgTGXKgB'),identifier(none,max_w),integer_set(none))]),theorems(none,[]),events(none,[event(rodinpos(conc_4,'INITIALISATION',internal_evt1),'INITIALISATION',ordinary(none),['INITIALISATION'],[],[],[],[assign(rodinpos(conc_4,act7,internal_act7),[identifier(none,adr_w)],[integer(none,1)]),assign(rodinpos(conc_4,act8,internal_act8),[identifier(none,adr_r)],[integer(none,1)]),assign(rodinpos(conc_4,act12,internal_act12),[identifier(none,y)],[identifier(none,d0)]),assign(rodinpos(conc_4,act2,internal_act2),[identifier(none,reading)],[integer(none,0)]),assign(rodinpos(conc_4,act3,internal_act3),[identifier(none,pair_w)],[integer(none,0)]),assign(rodinpos(conc_4,act4,internal_act4),[identifier(none,latest)],[integer(none,0)]),assign(rodinpos(conc_4,act5,internal_act5),[identifier(none,indx_r)],[integer(none,0)]),assign(rodinpos(conc_4,act6,internal_act6),[identifier(none,indx_w)],[integer(none,0)]),assign(rodinpos(conc_4,act13,internal_act13),[identifier(none,slot)],[set_extension(none,[couple(none,[integer(none,0),integer(none,0)]),couple(none,[integer(none,1),integer(none,0)])])]),assign(rodinpos(conc_4,act14,internal_act14),[identifier(none,data)],[set_extension(none,[couple(none,[integer(none,0),set_extension(none,[couple(none,[integer(none,0),identifier(none,d0)]),couple(none,[integer(none,1),identifier(none,d0)])])]),couple(none,[integer(none,1),set_extension(none,[couple(none,[integer(none,0),identifier(none,d0)]),couple(none,[integer(none,1),identifier(none,d0)])])])])]),becomes_element_of(rodinpos(conc_4,act1,internal_act1),[identifier(none,x)],identifier(none,'D')),assign(rodinpos(conc_4,act15,'_Zz5qIEDaEeWuxbRgTGXKgA'),[identifier(none,max_r)],[integer(none,0)]),assign(rodinpos(conc_4,act16,'_Zz5qIEDaEeWuxbRgTGXKgB'),[identifier(none,max_w)],[integer(none,0)])],[]),event(rodinpos(conc_4,'Reader_1',internal_evt4),'Reader_1',ordinary(none),['Reader_1'],[],[equal(rodinpos(conc_4,grd1,internal_grd1),identifier(none,adr_r),integer(none,1)),less(rodinpos(conc_4,grd2,'_xSHS8EDYEeWuxbRgTGXKgA'),identifier(none,max_r),identifier(none,max_steps))],[],[assign(rodinpos(conc_4,act1,'_Zz6RMEDaEeWuxbRgTGXKgA'),[identifier(none,adr_r)],[integer(none,2)]),assign(rodinpos(conc_4,act2,internal_act3),[identifier(none,reading)],[identifier(none,latest)])],[]),event(rodinpos(conc_4,'Reader_2',internal_evt3),'Reader_2',ordinary(none),['Reader_2'],[],[equal(rodinpos(conc_4,grd1,internal_grd1),identifier(none,adr_r),integer(none,2))],[],[assign(rodinpos(conc_4,act2,internal_act1),[identifier(none,indx_r)],[function(none,identifier(none,slot),[identifier(none,reading)])]),assign(rodinpos(conc_4,act3,internal_act2),[identifier(none,adr_r)],[integer(none,3)])],[]),event(rodinpos(conc_4,'Reader_3',internal_evt5),'Reader_3',ordinary(none),['Reader_3'],[],[equal(rodinpos(conc_4,grd1,internal_grd2),identifier(none,adr_r),integer(none,3))],[],[assign(rodinpos(conc_4,act1,'_cChjMEDtEeWuxbRgTGXKgA'),[identifier(none,y)],[function(none,function(none,identifier(none,data),[identifier(none,reading)]),[identifier(none,indx_r)])]),assign(rodinpos(conc_4,act2,'_zrbTsEDYEeWuxbRgTGXKgA'),[identifier(none,adr_r)],[integer(none,1)]),assign(rodinpos(conc_4,act3,internal_act3),[identifier(none,max_r)],[add(none,identifier(none,max_r),integer(none,1))])],[]),event(rodinpos(conc_4,'Writer_1',internal_evt2),'Writer_1',ordinary(none),['Writer_1'],[identifier(rodinpos(conc_4,[],internal_var1),d)],[member(rodinpos(conc_4,grd1,internal_grd1),identifier(none,d),identifier(none,'D')),equal(rodinpos(conc_4,grd2,'_aY22sEDtEeWuxbRgTGXKgA'),identifier(none,adr_w),integer(none,1)),less(rodinpos(conc_4,grd3,'_2_aM8EDYEeWuxbRgTGXKgA'),identifier(none,max_w),identifier(none,max_steps))],[],[assign(rodinpos(conc_4,act2,internal_act2),[identifier(none,adr_w)],[integer(none,2)]),assign(rodinpos(conc_4,act3,internal_act5),[identifier(none,pair_w)],[minus(none,integer(none,1),identifier(none,reading))]),assign(rodinpos(conc_4,act5,'_iH3JwEDtEeWuxbRgTGXKgA'),[identifier(none,x)],[identifier(none,d)])],[]),event(rodinpos(conc_4,'Writer_2',internal_evt7),'Writer_2',ordinary(none),['Writer_2'],[],[equal(rodinpos(conc_4,grd1,internal_grd1),identifier(none,adr_w),integer(none,2))],[],[assign(rodinpos(conc_4,act1,'_bch00EDaEeWuxbRgTGXKgA'),[identifier(none,adr_w)],[integer(none,3)]),assign(rodinpos(conc_4,act2,internal_act2),[identifier(none,indx_w)],[minus(none,integer(none,1),function(none,identifier(none,slot),[identifier(none,pair_w)]))])],[]),event(rodinpos(conc_4,'Writer_3',internal_evt8),'Writer_3',ordinary(none),['Writer_3'],[],[equal(rodinpos(conc_4,grd1,internal_grd1),identifier(none,adr_w),integer(none,3))],[],[assign(rodinpos(conc_4,act1,internal_act1),[identifier(none,adr_w)],[integer(none,4)]),assign(rodinpos(conc_4,act2,internal_act2),[identifier(none,data)],[overwrite(none,identifier(none,data),set_extension(none,[couple(none,[identifier(none,pair_w),overwrite(none,function(none,identifier(none,data),[identifier(none,pair_w)]),set_extension(none,[couple(none,[identifier(none,indx_w),identifier(none,x)])]))])]))])],[]),event(rodinpos(conc_4,'Writer_4',internal_evt10),'Writer_4',ordinary(none),['Writer_41','Writer_42'],[],[equal(rodinpos(conc_4,grd1,'_YLnjEEDtEeWuxbRgTGXKgA'),identifier(none,adr_w),integer(none,4))],[],[assign(rodinpos(conc_4,act1,internal_act1),[identifier(none,adr_w)],[integer(none,5)]),assign(rodinpos(conc_4,act2,'_cCiKQEDtEeWuxbRgTGXKgA'),[identifier(none,slot)],[overwrite(none,identifier(none,slot),set_extension(none,[couple(none,[identifier(none,pair_w),identifier(none,indx_w)])]))])],[]),event(rodinpos(conc_4,'Writer_5',internal_evt6),'Writer_5',ordinary(none),['Writer_51','Writer_52'],[],[equal(rodinpos(conc_4,grd1,'_YLnjEUDtEeWuxbRgTGXKgA'),identifier(none,adr_w),integer(none,5))],[],[assign(rodinpos(conc_4,act1,'_iH3w0EDtEeWuxbRgTGXKgA'),[identifier(none,adr_w)],[integer(none,1)]),assign(rodinpos(conc_4,act2,'_iH3w0EDtEeWuxbRgTGXKgB'),[identifier(none,max_w)],[add(none,identifier(none,max_w),integer(none,1))]),assign(rodinpos(conc_4,act3,'_iH3w0EDtEeWuxbRgTGXKgC'),[identifier(none,latest)],[identifier(none,pair_w)])],[]),event(rodinpos(conc_4,stopped_read,'_xmnosEDrEeWuxbRgTGXKgA'),stopped_read,ordinary(none),[stopped_read],[],[equal(rodinpos(conc_4,grd1,'_aY4r4EDtEeWuxbRgTGXKgA'),identifier(none,max_r),identifier(none,max_steps))],[],[],[]),event(rodinpos(conc_4,stopped_write,'_xmoPwEDrEeWuxbRgTGXKgA'),stopped_write,ordinary(none),[stopped_write],[],[equal(rodinpos(conc_4,grd1,'_eUygwEDtEeWuxbRgTGXKgA'),identifier(none,max_w),identifier(none,max_steps))],[],[],[])])]),event_b_model(none,conc_3,[sees(none,[conc_ctx_0]),refines(none,conc_2),variables(none,[identifier(none,'Data'),identifier(none,adr_r),identifier(none,adr_w),identifier(none,indx_r),identifier(none,indx_wp),identifier(none,latest),identifier(none,max_r),identifier(none,max_w),identifier(none,pair_w),identifier(none,reading),identifier(none,slot),identifier(none,y)]),invariant(none,[member(rodinpos(conc_3,inv1,internal_inv1I),identifier(none,'Data'),total_function(none,set_extension(none,[integer(none,0),integer(none,1)]),total_function(none,set_extension(none,[integer(none,0),integer(none,1)]),identifier(none,'D')))),forall(rodinpos(conc_3,inv2,internal_inv2I),[identifier(none,x),identifier(none,z)],implication(none,conjunct(none,member(none,identifier(none,x),integer_set(none)),conjunct(none,member(none,identifier(none,z),integer_set(none)),conjunct(none,member(none,identifier(none,x),set_extension(none,[integer(none,0),integer(none,1)])),member(none,identifier(none,z),set_extension(none,[integer(none,0),integer(none,1)]))))),equal(none,function(none,identifier(none,wtp),[function(none,function(none,identifier(none,idata),[identifier(none,x)]),[identifier(none,z)])]),function(none,function(none,identifier(none,'Data'),[identifier(none,x)]),[identifier(none,z)]))))]),theorems(none,[]),events(none,[event(rodinpos(conc_3,'INITIALISATION',internal_evt1),'INITIALISATION',ordinary(none),['INITIALISATION'],[],[],[],[assign(rodinpos(conc_3,act7,internal_act7),[identifier(none,adr_w)],[integer(none,1)]),assign(rodinpos(conc_3,act8,internal_act8),[identifier(none,adr_r)],[integer(none,1)]),assign(rodinpos(conc_3,act12,internal_act12),[identifier(none,y)],[identifier(none,d0)]),assign(rodinpos(conc_3,act2,internal_act2),[identifier(none,reading)],[integer(none,0)]),assign(rodinpos(conc_3,act3,internal_act3),[identifier(none,pair_w)],[integer(none,0)]),assign(rodinpos(conc_3,act4,internal_act4),[identifier(none,latest)],[integer(none,0)]),assign(rodinpos(conc_3,act5,internal_act5),[identifier(none,indx_r)],[integer(none,0)]),assign(rodinpos(conc_3,act6,internal_act6),[identifier(none,indx_wp)],[integer(none,0)]),assign(rodinpos(conc_3,act13,internal_act13),[identifier(none,slot)],[set_extension(none,[couple(none,[integer(none,0),integer(none,0)]),couple(none,[integer(none,1),integer(none,0)])])]),assign(rodinpos(conc_3,act14,internal_act14),[identifier(none,'Data')],[set_extension(none,[couple(none,[integer(none,0),set_extension(none,[couple(none,[integer(none,0),identifier(none,d0)]),couple(none,[integer(none,1),identifier(none,d0)])])]),couple(none,[integer(none,1),set_extension(none,[couple(none,[integer(none,0),identifier(none,d0)]),couple(none,[integer(none,1),identifier(none,d0)])])])])]),assign(rodinpos(conc_3,act15,internal_act1),[identifier(none,max_r)],[integer(none,0)]),assign(rodinpos(conc_3,act16,'_RmpaMEDtEeWuxbRgTGXKgA'),[identifier(none,max_w)],[integer(none,0)])],[]),event(rodinpos(conc_3,'Reader_1',internal_evt4),'Reader_1',ordinary(none),['Reader_1'],[],[equal(rodinpos(conc_3,grd1,internal_grd1),identifier(none,adr_r),integer(none,1)),less(rodinpos(conc_3,grd2,'_OdIEgEDtEeWuxbRgTGXKgA'),identifier(none,max_r),identifier(none,max_steps))],[],[assign(rodinpos(conc_3,act1,internal_act2),[identifier(none,adr_r)],[integer(none,2)]),assign(rodinpos(conc_3,act2,internal_act3),[identifier(none,reading)],[identifier(none,latest)])],[]),event(rodinpos(conc_3,'Reader_2',internal_evt3),'Reader_2',ordinary(none),['Reader_2'],[],[equal(rodinpos(conc_3,grd1,internal_grd1),identifier(none,adr_r),integer(none,2))],[],[assign(rodinpos(conc_3,act2,internal_act1),[identifier(none,indx_r)],[function(none,identifier(none,slot),[identifier(none,reading)])]),assign(rodinpos(conc_3,act3,internal_act2),[identifier(none,adr_r)],[integer(none,3)])],[]),event(rodinpos(conc_3,'Reader_3',internal_evt5),'Reader_3',ordinary(none),['Reader_3'],[],[equal(rodinpos(conc_3,grd1,internal_grd1),identifier(none,adr_r),integer(none,3))],[],[assign(rodinpos(conc_3,act1,'_MTamAEDtEeWuxbRgTGXKgA'),[identifier(none,y)],[function(none,function(none,identifier(none,'Data'),[identifier(none,reading)]),[identifier(none,indx_r)])]),assign(rodinpos(conc_3,act2,internal_act3),[identifier(none,adr_r)],[integer(none,1)]),assign(rodinpos(conc_3,act3,internal_act4),[identifier(none,max_r)],[add(none,identifier(none,max_r),integer(none,1))])],[]),event(rodinpos(conc_3,'Writer_1',internal_evt2),'Writer_1',ordinary(none),['Writer_1'],[identifier(rodinpos(conc_3,[],internal_var1),d)],[member(rodinpos(conc_3,grd1,internal_grd2),identifier(none,d),identifier(none,'D')),equal(rodinpos(conc_3,grd2,'_Kfo7QEDtEeWuxbRgTGXKgA'),identifier(none,adr_w),integer(none,1)),less(rodinpos(conc_3,grd3,internal_grd1),identifier(none,max_w),identifier(none,max_steps))],[],[assign(rodinpos(conc_3,act2,internal_act5),[identifier(none,adr_w)],[integer(none,2)]),assign(rodinpos(conc_3,act3,internal_act1),[identifier(none,pair_w)],[minus(none,integer(none,1),identifier(none,reading))]),assign(rodinpos(conc_3,act4,'_RmqoUEDtEeWuxbRgTGXKgA'),[identifier(none,indx_wp)],[minus(none,integer(none,1),function(none,identifier(none,slot),[minus(none,integer(none,1),identifier(none,reading))]))]),assign(rodinpos(conc_3,act5,'_RmqoUUDtEeWuxbRgTGXKgA'),[identifier(none,'Data')],[overwrite(none,identifier(none,'Data'),set_extension(none,[couple(none,[minus(none,integer(none,1),identifier(none,reading)),overwrite(none,function(none,identifier(none,'Data'),[minus(none,integer(none,1),identifier(none,reading))]),set_extension(none,[couple(none,[minus(none,integer(none,1),function(none,identifier(none,slot),[minus(none,integer(none,1),identifier(none,reading))])),identifier(none,d)])]))])]))])],[]),event(rodinpos(conc_3,'Writer_2',internal_evt7),'Writer_2',ordinary(none),['Writer_2'],[],[equal(rodinpos(conc_3,grd1,internal_grd1),identifier(none,adr_w),integer(none,2))],[],[assign(rodinpos(conc_3,act1,internal_act2),[identifier(none,adr_w)],[integer(none,3)])],[]),event(rodinpos(conc_3,'Writer_3',internal_evt8),'Writer_3',ordinary(none),['Writer_3'],[],[equal(rodinpos(conc_3,grd1,internal_grd2),identifier(none,adr_w),integer(none,3))],[],[assign(rodinpos(conc_3,act1,'_MTbNEEDtEeWuxbRgTGXKgA'),[identifier(none,adr_w)],[integer(none,4)])],[]),event(rodinpos(conc_3,'Writer_41',internal_evt9),'Writer_41',ordinary(none),['Writer_41'],[],[equal(rodinpos(conc_3,grd1,internal_grd1),identifier(none,adr_w),integer(none,4)),negation(rodinpos(conc_3,grd2,internal_grd2),equal(none,identifier(none,pair_w),identifier(none,latest)))],[],[assign(rodinpos(conc_3,act1,internal_act3),[identifier(none,adr_w)],[integer(none,5)]),assign(rodinpos(conc_3,act2,internal_act1),[identifier(none,slot)],[overwrite(none,identifier(none,slot),set_extension(none,[couple(none,[identifier(none,pair_w),identifier(none,indx_wp)])]))])],[]),event(rodinpos(conc_3,'Writer_42',internal_evt10),'Writer_42',ordinary(none),['Writer_42'],[],[equal(rodinpos(conc_3,grd1,internal_grd1),identifier(none,adr_w),integer(none,4)),equal(rodinpos(conc_3,grd2,internal_grd2),identifier(none,pair_w),identifier(none,latest))],[],[assign(rodinpos(conc_3,act1,internal_act2),[identifier(none,adr_w)],[integer(none,5)]),assign(rodinpos(conc_3,act2,'_GwP4YEDtEeWuxbRgTGXKgA'),[identifier(none,slot)],[overwrite(none,identifier(none,slot),set_extension(none,[couple(none,[identifier(none,pair_w),identifier(none,indx_wp)])]))])],[]),event(rodinpos(conc_3,'Writer_51',internal_evt6),'Writer_51',ordinary(none),['Writer_51'],[],[equal(rodinpos(conc_3,grd1,internal_grd1),identifier(none,adr_w),integer(none,5)),negation(rodinpos(conc_3,grd2,internal_grd2),equal(none,identifier(none,pair_w),identifier(none,latest)))],[],[assign(rodinpos(conc_3,act1,'_MTb0IEDtEeWuxbRgTGXKgA'),[identifier(none,adr_w)],[integer(none,1)]),assign(rodinpos(conc_3,act2,'_FUE1UEDtEeWuxbRgTGXKgA'),[identifier(none,latest)],[identifier(none,pair_w)]),assign(rodinpos(conc_3,act3,'_MTb0IEDtEeWuxbRgTGXKgB'),[identifier(none,max_w)],[add(none,identifier(none,max_w),integer(none,1))])],[]),event(rodinpos(conc_3,'Writer_52',internal_evt11),'Writer_52',ordinary(none),['Writer_52'],[],[equal(rodinpos(conc_3,grd1,'_Dqu48EDtEeWuxbRgTGXKgA'),identifier(none,adr_w),integer(none,5)),equal(rodinpos(conc_3,grd2,'_Dqu48UDtEeWuxbRgTGXKgA'),identifier(none,pair_w),identifier(none,latest))],[],[assign(rodinpos(conc_3,act1,'_MTb0IUDtEeWuxbRgTGXKgA'),[identifier(none,adr_w)],[integer(none,1)]),assign(rodinpos(conc_3,act2,'_RmrPYEDtEeWuxbRgTGXKgA'),[identifier(none,latest)],[identifier(none,pair_w)]),assign(rodinpos(conc_3,act3,'_Rmr2cEDtEeWuxbRgTGXKgA'),[identifier(none,max_w)],[add(none,identifier(none,max_w),integer(none,1))])],[]),event(rodinpos(conc_3,stopped_read,'_zgRR8EDrEeWuxbRgTGXKgA'),stopped_read,ordinary(none),[stopped_read],[],[equal(rodinpos(conc_3,grd1,'_KfqwcEDtEeWuxbRgTGXKgA'),identifier(none,max_r),identifier(none,max_steps))],[],[],[]),event(rodinpos(conc_3,stopped_write,'_zgRR8kDrEeWuxbRgTGXKgA'),stopped_write,ordinary(none),[stopped_write],[],[equal(rodinpos(conc_3,grd1,'_OdJ5sEDtEeWuxbRgTGXKgA'),identifier(none,max_w),identifier(none,max_steps))],[],[],[])])]),event_b_model(none,conc_2,[sees(none,[conc_ctx_0]),refines(none,conc_1),variables(none,[identifier(none,adr_r),identifier(none,adr_w),identifier(none,idata),identifier(none,indx_r),identifier(none,indx_wp),identifier(none,latest),identifier(none,max_r),identifier(none,max_w),identifier(none,pair_w),identifier(none,reading),identifier(none,slot),identifier(none,w),identifier(none,wtp),identifier(none,y)]),invariant(none,[member(rodinpos(conc_2,inv1,internal_inv1I),identifier(none,reading),set_extension(none,[integer(none,0),integer(none,1)])),member(rodinpos(conc_2,inv2,internal_inv2I),identifier(none,pair_w),set_extension(none,[integer(none,0),integer(none,1)])),member(rodinpos(conc_2,inv3,internal_inv3I),identifier(none,latest),set_extension(none,[integer(none,0),integer(none,1)])),member(rodinpos(conc_2,inv4,internal_inv4I),identifier(none,indx_r),set_extension(none,[integer(none,0),integer(none,1)])),member(rodinpos(conc_2,inv5,internal_inv5I),identifier(none,indx_wp),set_extension(none,[integer(none,0),integer(none,1)])),member(rodinpos(conc_2,inv6,internal_inv6I),identifier(none,slot),total_function(none,set_extension(none,[integer(none,0),integer(none,1)]),set_extension(none,[integer(none,0),integer(none,1)]))),member(rodinpos(conc_2,inv7,internal_inv7I),identifier(none,idata),total_function(none,set_extension(none,[integer(none,0),integer(none,1)]),total_function(none,set_extension(none,[integer(none,0),integer(none,1)]),domain(none,identifier(none,wtp))))),implication(rodinpos(conc_2,inv8,internal_inv8I),equal(none,identifier(none,adr_r),integer(none,2)),member(none,function(none,function(none,identifier(none,idata),[identifier(none,reading)]),[function(none,identifier(none,slot),[identifier(none,reading)])]),interval(none,identifier(none,u),identifier(none,w)))),implication(rodinpos(conc_2,inv9,internal_element1I),equal(none,identifier(none,adr_r),integer(none,3)),equal(none,identifier(none,m),function(none,function(none,identifier(none,idata),[identifier(none,reading)]),[identifier(none,indx_r)]))),equal(rodinpos(conc_2,inv10,internal_inv9I),function(none,function(none,identifier(none,idata),[identifier(none,latest)]),[function(none,identifier(none,slot),[identifier(none,latest)])]),identifier(none,w)),implication(rodinpos(conc_2,inv11,internal_inv10I),equal(none,identifier(none,adr_w),integer(none,1)),equal(none,identifier(none,pair_w),identifier(none,latest))),implication(rodinpos(conc_2,inv12,internal_inv11I),equal(none,identifier(none,reading),identifier(none,pair_w)),equal(none,identifier(none,latest),identifier(none,reading))),implication(rodinpos(conc_2,inv13,internal_inv12I),member(none,identifier(none,adr_w),set_extension(none,[integer(none,1),integer(none,5)])),equal(none,identifier(none,indx_wp),function(none,identifier(none,slot),[identifier(none,pair_w)]))),implication(rodinpos(conc_2,inv14,internal_inv13I),member(none,identifier(none,adr_w),set_extension(none,[integer(none,2),integer(none,3),integer(none,4)])),equal(none,identifier(none,indx_wp),minus(none,integer(none,1),function(none,identifier(none,slot),[identifier(none,pair_w)])))),implication(rodinpos(conc_2,inv15,internal_inv14I),conjunct(none,equal(none,identifier(none,adr_w),integer(none,5)),equal(none,identifier(none,latest),identifier(none,pair_w))),equal(none,domain(none,identifier(none,wtp)),interval(none,integer(none,1),identifier(none,w)))),implication(rodinpos(conc_2,inv16,internal_inv16I),conjunct(none,equal(none,identifier(none,adr_w),integer(none,5)),equal(none,domain(none,identifier(none,wtp)),interval(none,integer(none,1),identifier(none,w)))),equal(none,identifier(none,latest),identifier(none,pair_w))),equal(rodinpos(conc_2,inv17,internal_inv15I),function(none,function(none,identifier(none,idata),[identifier(none,pair_w)]),[identifier(none,indx_wp)]),max(none,domain(none,identifier(none,wtp)))),member(rodinpos(conc_2,inv18,internal_thm1T),identifier(none,max_r),integer_set(none)),member(rodinpos(conc_2,inv19,internal_thm2T),identifier(none,max_w),integer_set(none))]),theorems(none,[negation(rodinpos(conc_2,thm1,'_0CZ5MEDsEeWuxbRgTGXKgA'),equal(none,identifier(none,reading),minus(none,integer(none,1),identifier(none,reading)))),negation(rodinpos(conc_2,thm2,'_0CZ5MUDsEeWuxbRgTGXKgA'),equal(none,function(none,identifier(none,slot),[minus(none,integer(none,1),identifier(none,reading))]),minus(none,integer(none,1),function(none,identifier(none,slot),[minus(none,integer(none,1),identifier(none,reading))]))))]),events(none,[event(rodinpos(conc_2,'INITIALISATION',internal_evt1),'INITIALISATION',ordinary(none),['INITIALISATION'],[],[],[],[assign(rodinpos(conc_2,act7,internal_act7),[identifier(none,adr_w)],[integer(none,1)]),assign(rodinpos(conc_2,act8,internal_act8),[identifier(none,adr_r)],[integer(none,1)]),assign(rodinpos(conc_2,act11,internal_act11),[identifier(none,wtp)],[set_extension(none,[couple(none,[integer(none,1),identifier(none,d0)])])]),assign(rodinpos(conc_2,act12,internal_act12),[identifier(none,y)],[identifier(none,d0)]),assign(rodinpos(conc_2,act1,internal_act1),[identifier(none,w)],[integer(none,1)]),assign(rodinpos(conc_2,act2,internal_act2),[identifier(none,reading)],[integer(none,0)]),assign(rodinpos(conc_2,act3,internal_act3),[identifier(none,pair_w)],[integer(none,0)]),assign(rodinpos(conc_2,act4,internal_act4),[identifier(none,latest)],[integer(none,0)]),assign(rodinpos(conc_2,act5,internal_act5),[identifier(none,indx_r)],[integer(none,0)]),assign(rodinpos(conc_2,act6,internal_act6),[identifier(none,indx_wp)],[integer(none,0)]),assign(rodinpos(conc_2,act13,internal_act13),[identifier(none,slot)],[set_extension(none,[couple(none,[integer(none,0),integer(none,0)]),couple(none,[integer(none,1),integer(none,0)])])]),assign(rodinpos(conc_2,act14,internal_act14),[identifier(none,idata)],[set_extension(none,[couple(none,[integer(none,0),set_extension(none,[couple(none,[integer(none,0),integer(none,1)]),couple(none,[integer(none,1),integer(none,1)])])]),couple(none,[integer(none,1),set_extension(none,[couple(none,[integer(none,0),integer(none,1)]),couple(none,[integer(none,1),integer(none,1)])])])])]),assign(rodinpos(conc_2,act15,'_sql-IEDsEeWuxbRgTGXKgA'),[identifier(none,max_r)],[integer(none,0)]),assign(rodinpos(conc_2,act16,'_sql-IUDsEeWuxbRgTGXKgA'),[identifier(none,max_w)],[integer(none,0)])],[]),event(rodinpos(conc_2,'Reader_1',internal_evt4),'Reader_1',ordinary(none),['Reader_1'],[],[equal(rodinpos(conc_2,grd1,internal_grd1),identifier(none,adr_r),integer(none,1)),less(rodinpos(conc_2,grd2,'_BZAG4EDtEeWuxbRgTGXKgA'),identifier(none,max_r),identifier(none,max_steps))],[],[assign(rodinpos(conc_2,act1,internal_act2),[identifier(none,adr_r)],[integer(none,2)]),assign(rodinpos(conc_2,act2,internal_act3),[identifier(none,reading)],[identifier(none,latest)])],[]),event(rodinpos(conc_2,'Reader_2',internal_evt3),'Reader_2',ordinary(none),['Reader_2'],[],[equal(rodinpos(conc_2,grd1,internal_grd1),identifier(none,adr_r),integer(none,2))],[],[assign(rodinpos(conc_2,act2,internal_act1),[identifier(none,indx_r)],[function(none,identifier(none,slot),[identifier(none,reading)])]),assign(rodinpos(conc_2,act3,internal_act2),[identifier(none,adr_r)],[integer(none,3)])],[witness(none,identifier(none,v),equal(rodinpos(conc_2,v,internal_wit1),identifier(none,v),function(none,function(none,identifier(none,idata),[identifier(none,reading)]),[function(none,identifier(none,slot),[identifier(none,reading)])])))]),event(rodinpos(conc_2,'Reader_3',internal_evt5),'Reader_3',ordinary(none),['Reader_3'],[],[equal(rodinpos(conc_2,grd1,internal_grd1),identifier(none,adr_r),integer(none,3))],[],[assign(rodinpos(conc_2,act1,internal_act1),[identifier(none,y)],[function(none,identifier(none,wtp),[function(none,function(none,identifier(none,idata),[identifier(none,reading)]),[identifier(none,indx_r)])])]),assign(rodinpos(conc_2,act2,internal_act2),[identifier(none,adr_r)],[integer(none,1)]),assign(rodinpos(conc_2,act3,internal_act3),[identifier(none,max_r)],[add(none,identifier(none,max_r),integer(none,1))])],[]),event(rodinpos(conc_2,'Writer_1',internal_evt2),'Writer_1',ordinary(none),['Writer_1'],[identifier(rodinpos(conc_2,[],internal_var1),d)],[member(rodinpos(conc_2,grd1,internal_grd2),identifier(none,d),identifier(none,'D')),equal(rodinpos(conc_2,grd2,'_97O_gEDsEeWuxbRgTGXKgA'),identifier(none,adr_w),integer(none,1)),less(rodinpos(conc_2,grd3,internal_grd1),identifier(none,max_w),identifier(none,max_steps))],[],[assign(rodinpos(conc_2,act1,internal_act4),[identifier(none,wtp)],[overwrite(none,identifier(none,wtp),set_extension(none,[couple(none,[add(none,identifier(none,w),integer(none,1)),identifier(none,d)])]))]),assign(rodinpos(conc_2,act2,internal_act5),[identifier(none,adr_w)],[integer(none,2)]),assign(rodinpos(conc_2,act3,internal_act1),[identifier(none,pair_w)],[minus(none,integer(none,1),identifier(none,reading))]),assign(rodinpos(conc_2,act4,'_sqoaYEDsEeWuxbRgTGXKgA'),[identifier(none,indx_wp)],[minus(none,integer(none,1),function(none,identifier(none,slot),[minus(none,integer(none,1),identifier(none,reading))]))]),assign(rodinpos(conc_2,act5,'__ucCgEDsEeWuxbRgTGXKgA'),[identifier(none,idata)],[overwrite(none,identifier(none,idata),set_extension(none,[couple(none,[minus(none,integer(none,1),identifier(none,reading)),overwrite(none,function(none,identifier(none,idata),[minus(none,integer(none,1),identifier(none,reading))]),set_extension(none,[couple(none,[minus(none,integer(none,1),function(none,identifier(none,slot),[minus(none,integer(none,1),identifier(none,reading))])),add(none,identifier(none,w),integer(none,1))])]))])]))])],[]),event(rodinpos(conc_2,'Writer_2',internal_evt7),'Writer_2',ordinary(none),['Writer_2'],[],[equal(rodinpos(conc_2,grd1,internal_grd1),identifier(none,adr_w),integer(none,2))],[],[assign(rodinpos(conc_2,act1,internal_act2),[identifier(none,adr_w)],[integer(none,3)])],[]),event(rodinpos(conc_2,'Writer_3',internal_evt8),'Writer_3',ordinary(none),['Writer_3'],[],[equal(rodinpos(conc_2,grd1,internal_grd2),identifier(none,adr_w),integer(none,3))],[],[assign(rodinpos(conc_2,act1,internal_act1),[identifier(none,adr_w)],[integer(none,4)])],[]),event(rodinpos(conc_2,'Writer_41',internal_evt9),'Writer_41',ordinary(none),['Writer_41'],[],[equal(rodinpos(conc_2,grd1,internal_grd1),identifier(none,adr_w),integer(none,4)),negation(rodinpos(conc_2,grd2,internal_grd2),equal(none,identifier(none,pair_w),identifier(none,latest)))],[],[assign(rodinpos(conc_2,act1,internal_act2),[identifier(none,adr_w)],[integer(none,5)]),assign(rodinpos(conc_2,act2,internal_act3),[identifier(none,slot)],[overwrite(none,identifier(none,slot),set_extension(none,[couple(none,[identifier(none,pair_w),identifier(none,indx_wp)])]))])],[]),event(rodinpos(conc_2,'Writer_42',internal_evt10),'Writer_42',ordinary(none),['Writer_42'],[],[equal(rodinpos(conc_2,grd1,internal_grd1),identifier(none,adr_w),integer(none,4)),equal(rodinpos(conc_2,grd2,internal_grd2),identifier(none,pair_w),identifier(none,latest))],[],[assign(rodinpos(conc_2,act1,internal_act1),[identifier(none,w)],[add(none,identifier(none,w),integer(none,1))]),assign(rodinpos(conc_2,act2,internal_act2),[identifier(none,adr_w)],[integer(none,5)]),assign(rodinpos(conc_2,act3,internal_act3),[identifier(none,slot)],[overwrite(none,identifier(none,slot),set_extension(none,[couple(none,[identifier(none,pair_w),identifier(none,indx_wp)])]))])],[]),event(rodinpos(conc_2,'Writer_51',internal_evt11),'Writer_51',ordinary(none),['Writer_51'],[],[equal(rodinpos(conc_2,grd1,internal_grd1),identifier(none,adr_w),integer(none,5)),negation(rodinpos(conc_2,grd2,internal_grd2),equal(none,identifier(none,pair_w),identifier(none,latest)))],[],[assign(rodinpos(conc_2,act1,internal_act1),[identifier(none,w)],[add(none,identifier(none,w),integer(none,1))]),assign(rodinpos(conc_2,act2,internal_act2),[identifier(none,adr_w)],[integer(none,1)]),assign(rodinpos(conc_2,act3,'_sqpogEDsEeWuxbRgTGXKgA'),[identifier(none,latest)],[identifier(none,pair_w)]),assign(rodinpos(conc_2,act4,'_sqpogUDsEeWuxbRgTGXKgA'),[identifier(none,max_w)],[add(none,identifier(none,max_w),integer(none,1))])],[]),event(rodinpos(conc_2,'Writer_52',internal_evt12),'Writer_52',ordinary(none),['Writer_52'],[],[equal(rodinpos(conc_2,grd1,'_hOwM8EDsEeWuxbRgTGXKgA'),identifier(none,adr_w),integer(none,5)),equal(rodinpos(conc_2,grd2,'_kPTM0EDsEeWuxbRgTGXKgA'),identifier(none,pair_w),identifier(none,latest))],[],[assign(rodinpos(conc_2,act1,'_7ydVIEDsEeWuxbRgTGXKgA'),[identifier(none,adr_w)],[integer(none,1)]),assign(rodinpos(conc_2,act2,'_7ydVIUDsEeWuxbRgTGXKgA'),[identifier(none,latest)],[identifier(none,pair_w)]),assign(rodinpos(conc_2,act3,'__udQoEDsEeWuxbRgTGXKgA'),[identifier(none,max_w)],[add(none,identifier(none,max_w),integer(none,1))])],[]),event(rodinpos(conc_2,stopped_read,'_3MkkkEDrEeWuxbRgTGXKgA'),stopped_read,ordinary(none),[stopped_read],[],[equal(rodinpos(conc_2,grd1,'_97RbwEDsEeWuxbRgTGXKgA'),identifier(none,max_r),identifier(none,max_steps))],[],[],[]),event(rodinpos(conc_2,stopped_write,'_3MkkkkDrEeWuxbRgTGXKgA'),stopped_write,ordinary(none),[stopped_write],[],[equal(rodinpos(conc_2,grd1,'_BZDKMEDtEeWuxbRgTGXKgA'),identifier(none,max_w),identifier(none,max_steps))],[],[],[])])]),event_b_model(none,conc_1,[sees(none,[conc_ctx_0]),refines(none,conc_0),variables(none,[identifier(none,adr_r),identifier(none,adr_w),identifier(none,m),identifier(none,max_r),identifier(none,max_w),identifier(none,u),identifier(none,w),identifier(none,wtp),identifier(none,y)]),invariant(none,[member(rodinpos(conc_1,inv1,internal_inv1I),identifier(none,adr_w),set_extension(none,[integer(none,1),integer(none,2),integer(none,3),integer(none,4),integer(none,5)])),member(rodinpos(conc_1,inv2,internal_inv2I),identifier(none,adr_r),set_extension(none,[integer(none,1),integer(none,2),integer(none,3)])),equal(rodinpos(conc_1,inv3,internal_inv3I),identifier(none,u),function(none,identifier(none,g),[identifier(none,r)])),equal(rodinpos(conc_1,inv4,internal_inv4I),identifier(none,m),function(none,identifier(none,f),[identifier(none,r)])),member(rodinpos(conc_1,inv5,internal_inv5I),identifier(none,wtp),partial_function(none,natural1_set(none),identifier(none,'D'))),member(rodinpos(conc_1,inv6,internal_inv6I),identifier(none,y),identifier(none,'D')),implication(rodinpos(conc_1,inv7,internal_inv7I),equal(none,identifier(none,adr_r),integer(none,1)),equal(none,identifier(none,y),function(none,identifier(none,rd),[identifier(none,r)]))),subset(rodinpos(conc_1,inv8,internal_inv8I),identifier(none,wt),identifier(none,wtp)),implication(rodinpos(conc_1,inv9,internal_inv9I),equal(none,identifier(none,adr_w),integer(none,1)),equal(none,domain(none,identifier(none,wtp)),interval(none,integer(none,1),identifier(none,w)))),implication(rodinpos(conc_1,inv10,internal_inv10I),member(none,identifier(none,adr_w),set_extension(none,[integer(none,2),integer(none,3),integer(none,4)])),equal(none,domain(none,identifier(none,wtp)),interval(none,integer(none,1),add(none,identifier(none,w),integer(none,1))))),implication(rodinpos(conc_1,inv11,internal_inv11I),equal(none,identifier(none,adr_w),integer(none,5)),member(none,domain(none,identifier(none,wtp)),set_extension(none,[interval(none,integer(none,1),identifier(none,w)),interval(none,integer(none,1),add(none,identifier(none,w),integer(none,1)))]))),member(rodinpos(conc_1,inv12,'_aDJ-YEDrEeWuxbRgTGXKgA'),identifier(none,max_r),integer_set(none)),member(rodinpos(conc_1,inv13,'_aDJ-YUDrEeWuxbRgTGXKgA'),identifier(none,max_w),integer_set(none))]),theorems(none,[]),events(none,[event(rodinpos(conc_1,'INITIALISATION',internal_evt1),'INITIALISATION',ordinary(none),['INITIALISATION'],[],[],[],[assign(rodinpos(conc_1,act7,internal_act7),[identifier(none,adr_w)],[integer(none,1)]),assign(rodinpos(conc_1,act8,internal_act8),[identifier(none,adr_r)],[integer(none,1)]),assign(rodinpos(conc_1,act9,internal_act9),[identifier(none,u)],[integer(none,1)]),assign(rodinpos(conc_1,act10,internal_act10),[identifier(none,m)],[integer(none,1)]),assign(rodinpos(conc_1,act11,internal_act11),[identifier(none,wtp)],[set_extension(none,[couple(none,[integer(none,1),identifier(none,d0)])])]),assign(rodinpos(conc_1,act12,internal_act12),[identifier(none,y)],[identifier(none,d0)]),assign(rodinpos(conc_1,act1,internal_act1),[identifier(none,w)],[integer(none,1)]),assign(rodinpos(conc_1,act15,'_ehDGAEDrEeWuxbRgTGXKgA'),[identifier(none,max_r)],[integer(none,0)]),assign(rodinpos(conc_1,act16,'_ehDtEEDrEeWuxbRgTGXKgA'),[identifier(none,max_w)],[integer(none,0)])],[]),event(rodinpos(conc_1,'Reader_1',internal_evt4),'Reader_1',ordinary(none),[],[],[equal(rodinpos(conc_1,grd1,internal_grd1),identifier(none,adr_r),integer(none,1)),less(rodinpos(conc_1,grd2,'_Ys6kMEDrEeWuxbRgTGXKgA'),identifier(none,max_r),identifier(none,max_steps))],[],[assign(rodinpos(conc_1,act1,internal_act2),[identifier(none,adr_r)],[integer(none,2)])],[]),event(rodinpos(conc_1,'Reader_2',internal_evt3),'Reader_2',ordinary(none),[read],[identifier(rodinpos(conc_1,[],internal_var1),v)],[equal(rodinpos(conc_1,grd1,internal_grd2),identifier(none,adr_r),integer(none,2)),member(rodinpos(conc_1,grd2,internal_grd1),identifier(none,v),interval(none,identifier(none,u),identifier(none,w)))],[],[assign(rodinpos(conc_1,act1,internal_act3),[identifier(none,m)],[identifier(none,v)]),assign(rodinpos(conc_1,act2,internal_act1),[identifier(none,u)],[identifier(none,w)]),assign(rodinpos(conc_1,act3,internal_act2),[identifier(none,adr_r)],[integer(none,3)])],[]),event(rodinpos(conc_1,'Reader_3',internal_evt5),'Reader_3',ordinary(none),[],[],[equal(rodinpos(conc_1,grd1,internal_grd1),identifier(none,adr_r),integer(none,3))],[],[assign(rodinpos(conc_1,act1,'_WSTi8EDrEeWuxbRgTGXKgA'),[identifier(none,y)],[function(none,identifier(none,wtp),[identifier(none,m)])]),assign(rodinpos(conc_1,act2,internal_act2),[identifier(none,adr_r)],[integer(none,1)]),assign(rodinpos(conc_1,act3,internal_act1),[identifier(none,max_r)],[add(none,identifier(none,max_r),integer(none,1))])],[]),event(rodinpos(conc_1,'Writer_1',internal_evt2),'Writer_1',ordinary(none),[],[identifier(rodinpos(conc_1,[],internal_var1),d)],[member(rodinpos(conc_1,grd1,internal_grd2),identifier(none,d),identifier(none,'D')),equal(rodinpos(conc_1,grd2,'_SUPK4EDrEeWuxbRgTGXKgA'),identifier(none,adr_w),integer(none,1)),less(rodinpos(conc_1,grd3,internal_grd1),identifier(none,max_w),identifier(none,max_steps))],[],[assign(rodinpos(conc_1,act1,internal_act1),[identifier(none,wtp)],[overwrite(none,identifier(none,wtp),set_extension(none,[couple(none,[add(none,identifier(none,w),integer(none,1)),identifier(none,d)])]))]),assign(rodinpos(conc_1,act2,'_ehE7MEDrEeWuxbRgTGXKgA'),[identifier(none,adr_w)],[integer(none,2)])],[]),event(rodinpos(conc_1,'Writer_2',internal_evt7),'Writer_2',ordinary(none),[],[],[equal(rodinpos(conc_1,grd1,internal_grd1),identifier(none,adr_w),integer(none,2))],[],[assign(rodinpos(conc_1,act1,internal_act1),[identifier(none,adr_w)],[integer(none,3)])],[]),event(rodinpos(conc_1,'Writer_3',internal_evt8),'Writer_3',ordinary(none),[],[],[equal(rodinpos(conc_1,grd1,internal_grd1),identifier(none,adr_w),integer(none,3))],[],[assign(rodinpos(conc_1,act1,internal_act2),[identifier(none,adr_w)],[integer(none,4)])],[]),event(rodinpos(conc_1,'Writer_41',internal_evt9),'Writer_41',ordinary(none),[],[],[equal(rodinpos(conc_1,grd1,internal_grd1),identifier(none,adr_w),integer(none,4))],[],[assign(rodinpos(conc_1,act1,internal_act1),[identifier(none,adr_w)],[integer(none,5)])],[]),event(rodinpos(conc_1,'Writer_42',internal_evt10),'Writer_42',ordinary(none),[write],[],[equal(rodinpos(conc_1,grd1,internal_grd2),identifier(none,adr_w),integer(none,4))],[],[assign(rodinpos(conc_1,act1,internal_act2),[identifier(none,w)],[add(none,identifier(none,w),integer(none,1))]),assign(rodinpos(conc_1,act2,internal_act1),[identifier(none,adr_w)],[integer(none,5)])],[witness(none,identifier(none,d),equal(rodinpos(conc_1,d,internal_wit1),identifier(none,d),function(none,identifier(none,wtp),[add(none,identifier(none,w),integer(none,1))])))]),event(rodinpos(conc_1,'Writer_51',internal_evt11),'Writer_51',ordinary(none),[write],[],[equal(rodinpos(conc_1,grd1,internal_grd1),identifier(none,adr_w),integer(none,5)),equal(rodinpos(conc_1,grd2,internal_grd2),domain(none,identifier(none,wtp)),interval(none,integer(none,1),add(none,identifier(none,w),integer(none,1))))],[],[assign(rodinpos(conc_1,act1,'_OG-gQEDrEeWuxbRgTGXKgA'),[identifier(none,w)],[add(none,identifier(none,w),integer(none,1))]),assign(rodinpos(conc_1,act2,'_WSVYIEDrEeWuxbRgTGXKgA'),[identifier(none,adr_w)],[integer(none,1)]),assign(rodinpos(conc_1,act3,'_ehFiQEDrEeWuxbRgTGXKgA'),[identifier(none,max_w)],[add(none,identifier(none,max_w),integer(none,1))])],[witness(none,identifier(none,d),equal(rodinpos(conc_1,d,internal_wit1),identifier(none,d),function(none,identifier(none,wtp),[add(none,identifier(none,w),integer(none,1))])))]),event(rodinpos(conc_1,'Writer_52',internal_evt12),'Writer_52',ordinary(none),[],[],[equal(rodinpos(conc_1,grd1,'_J6DM0UDrEeWuxbRgTGXKgA'),identifier(none,adr_w),integer(none,5)),equal(rodinpos(conc_1,grd2,'_J6Dz4EDrEeWuxbRgTGXKgA'),domain(none,identifier(none,wtp)),interval(none,integer(none,1),identifier(none,w)))],[],[assign(rodinpos(conc_1,act1,'_ehFiQUDrEeWuxbRgTGXKgA'),[identifier(none,adr_w)],[integer(none,1)]),assign(rodinpos(conc_1,act3,'_hTf_gEDrEeWuxbRgTGXKgA'),[identifier(none,max_w)],[add(none,identifier(none,max_w),integer(none,1))])],[]),event(rodinpos(conc_1,stopped_read,'_J6DM0EDrEeWuxbRgTGXKgA'),stopped_read,ordinary(none),[],[],[equal(rodinpos(conc_1,grd1,'_SUUDYEDrEeWuxbRgTGXKgA'),identifier(none,max_r),identifier(none,max_steps))],[],[],[]),event(rodinpos(conc_1,stopped_write,'_J6DM0kDrEeWuxbRgTGXKgA'),stopped_write,ordinary(none),[],[],[equal(rodinpos(conc_1,grd2,'_Ys9ngEDrEeWuxbRgTGXKgA'),identifier(none,max_w),identifier(none,max_steps))],[],[],[])])]),event_b_model(none,conc_0,[sees(none,[conc_ctx_0]),variables(none,[identifier(none,f),identifier(none,g),identifier(none,r),identifier(none,rd),identifier(none,w),identifier(none,wt)]),invariant(none,[member(rodinpos(conc_0,inv1,internal_inv1I),identifier(none,w),natural1_set(none)),member(rodinpos(conc_0,inv2,internal_inv2I),identifier(none,r),natural1_set(none)),member(rodinpos(conc_0,inv3,internal_inv3I),identifier(none,wt),total_function(none,interval(none,integer(none,1),identifier(none,w)),identifier(none,'D'))),member(rodinpos(conc_0,inv4,internal_inv4I),identifier(none,rd),total_function(none,interval(none,integer(none,1),identifier(none,r)),identifier(none,'D'))),member(rodinpos(conc_0,inv5,internal_inv5I),identifier(none,f),total_function(none,interval(none,integer(none,1),identifier(none,r)),interval(none,integer(none,1),identifier(none,w)))),member(rodinpos(conc_0,inv6,internal_inv6I),identifier(none,g),total_function(none,interval(none,integer(none,1),identifier(none,r)),interval(none,integer(none,1),identifier(none,w)))),equal(rodinpos(conc_0,inv7,internal_inv7I),identifier(none,rd),composition(none,identifier(none,f),identifier(none,wt))),forall(rodinpos(conc_0,inv8,internal_inv8I),[identifier(none,i)],implication(none,conjunct(none,member(none,identifier(none,i),integer_set(none)),member(none,identifier(none,i),interval(none,integer(none,1),identifier(none,r)))),less_equal(none,function(none,identifier(none,f),[identifier(none,i)]),function(none,identifier(none,g),[identifier(none,i)])))),forall(rodinpos(conc_0,inv9,internal_inv9I),[identifier(none,i)],implication(none,conjunct(none,member(none,identifier(none,i),integer_set(none)),member(none,identifier(none,i),interval(none,integer(none,1),minus(none,identifier(none,r),integer(none,1))))),less_equal(none,function(none,identifier(none,g),[identifier(none,i)]),function(none,identifier(none,f),[add(none,identifier(none,i),integer(none,1))]))))]),theorems(none,[]),events(none,[event(rodinpos(conc_0,'INITIALISATION',internal_evt1),'INITIALISATION',ordinary(none),[],[],[],[],[assign(rodinpos(conc_0,act1,internal_act1),[identifier(none,w)],[integer(none,1)]),assign(rodinpos(conc_0,act2,internal_act2),[identifier(none,r)],[integer(none,1)]),assign(rodinpos(conc_0,act3,internal_act3),[identifier(none,wt)],[set_extension(none,[couple(none,[integer(none,1),identifier(none,d0)])])]),assign(rodinpos(conc_0,act4,internal_act4),[identifier(none,rd)],[set_extension(none,[couple(none,[integer(none,1),identifier(none,d0)])])]),assign(rodinpos(conc_0,act5,internal_act5),[identifier(none,f)],[set_extension(none,[couple(none,[integer(none,1),integer(none,1)])])]),assign(rodinpos(conc_0,act6,internal_act6),[identifier(none,g)],[set_extension(none,[couple(none,[integer(none,1),integer(none,1)])])])],[]),event(rodinpos(conc_0,write,internal_evt2),write,ordinary(none),[],[identifier(rodinpos(conc_0,[],internal_var1),d)],[member(rodinpos(conc_0,grd1,internal_grd1),identifier(none,d),identifier(none,'D'))],[],[assign(rodinpos(conc_0,act1,internal_act1),[identifier(none,w)],[add(none,identifier(none,w),integer(none,1))]),assign(rodinpos(conc_0,act2,internal_act2),[identifier(none,wt)],[overwrite(none,identifier(none,wt),set_extension(none,[couple(none,[add(none,identifier(none,w),integer(none,1)),identifier(none,d)])]))])],[]),event(rodinpos(conc_0,read,internal_evt3),read,ordinary(none),[],[identifier(rodinpos(conc_0,[],internal_var1),v)],[member(rodinpos(conc_0,grd1,'_h6qkoEDUEeWuxbRgTGXKgA'),identifier(none,v),interval(none,function(none,identifier(none,g),[identifier(none,r)]),identifier(none,w)))],[],[assign(rodinpos(conc_0,act1,internal_act1),[identifier(none,r)],[add(none,identifier(none,r),integer(none,1))]),assign(rodinpos(conc_0,act2,internal_act2),[identifier(none,f)],[overwrite(none,identifier(none,f),set_extension(none,[couple(none,[add(none,identifier(none,r),integer(none,1)),identifier(none,v)])]))]),assign(rodinpos(conc_0,act3,internal_act3),[identifier(none,g)],[overwrite(none,identifier(none,g),set_extension(none,[couple(none,[add(none,identifier(none,r),integer(none,1)),identifier(none,w)])]))]),assign(rodinpos(conc_0,act4,internal_act4),[identifier(none,rd)],[overwrite(none,identifier(none,rd),set_extension(none,[couple(none,[add(none,identifier(none,r),integer(none,1)),function(none,identifier(none,wt),[identifier(none,v)])])]))])],[])])])],[event_b_context(none,conc_ctx_0,[extends(none,[]),constants(none,[identifier(none,d0),identifier(none,max_steps)]),abstract_constants(none,[]),axioms(none,[member(rodinpos(conc_ctx_0,axm1,internal_axm1A),identifier(none,d0),identifier(none,'D')),equal(rodinpos(conc_ctx_0,axm2,'_m4cT8EDZEeWuxbRgTGXKgA'),identifier(none,max_steps),integer(none,4))]),theorems(none,[]),sets(none,[deferred_set(none,'D')])])],[exporter_version(3),po(conc_4,'Well-definedness of Invariant',[invariant(inv5)],true),po(conc_4,'Invariant establishment',[event('INITIALISATION'),event('INITIALISATION'),invariant(inv2)],false),po(conc_4,'Invariant establishment',[event('INITIALISATION'),event('INITIALISATION'),invariant(inv3)],true),po(conc_4,'Invariant establishment',[event('INITIALISATION'),event('INITIALISATION'),invariant(inv4)],true),po(conc_4,'Invariant establishment',[event('INITIALISATION'),event('INITIALISATION'),invariant(inv5)],false),po(conc_4,'Invariant establishment',[event('INITIALISATION'),event('INITIALISATION'),invariant(inv6)],true),po(conc_4,'Invariant establishment',[event('INITIALISATION'),event('INITIALISATION'),invariant(inv7)],true),po(conc_4,'Invariant establishment',[event('INITIALISATION'),event('INITIALISATION'),invariant(inv8)],true),po(conc_4,'Feasibility of action',[action(act1)],true),po(conc_4,'Action simulation',[event('INITIALISATION'),action(act13),event('INITIALISATION')],true),po(conc_4,'Action simulation',[event('INITIALISATION'),action(act16),event('INITIALISATION')],true),po(conc_4,'Invariant preservation',[event('Reader_1'),event('Reader_1'),invariant(inv7)],true),po(conc_4,'Invariant preservation',[event('Reader_1'),event('Reader_1'),invariant(inv8)],true),po(conc_4,'Invariant preservation',[event('Reader_2'),event('Reader_2'),invariant(inv7)],false),po(conc_4,'Invariant preservation',[event('Reader_2'),event('Reader_2'),invariant(inv8)],false),po(conc_4,'Invariant preservation',[event('Reader_3'),event('Reader_3'),invariant(inv7)],true),po(conc_4,'Invariant preservation',[event('Reader_3'),event('Reader_3'),invariant(inv8)],true),po(conc_4,'Well-definedness of action',[action(act1)],true),po(conc_4,'Action simulation',[event('Reader_3'),action(act1),event('Reader_3')],false),po(conc_4,'Invariant preservation',[event('Writer_1'),event('Writer_1'),invariant(inv4)],false),po(conc_4,'Invariant preservation',[event('Writer_1'),event('Writer_1'),invariant(inv5)],false),po(conc_4,'Invariant preservation',[event('Writer_1'),event('Writer_1'),invariant(inv6)],false),po(conc_4,'Invariant preservation',[event('Writer_1'),event('Writer_1'),invariant(inv7)],true),po(conc_4,'Invariant preservation',[event('Writer_1'),event('Writer_1'),invariant(inv8)],true),po(conc_4,'Invariant preservation',[event('Writer_2'),event('Writer_2'),invariant(inv3)],false),po(conc_4,'Invariant preservation',[event('Writer_2'),event('Writer_2'),invariant(inv4)],false),po(conc_4,'Invariant preservation',[event('Writer_2'),event('Writer_2'),invariant(inv5)],true),po(conc_4,'Invariant preservation',[event('Writer_2'),event('Writer_2'),invariant(inv6)],false),po(conc_4,'Invariant preservation',[event('Writer_2'),event('Writer_2'),invariant(inv7)],true),po(conc_4,'Invariant preservation',[event('Writer_2'),event('Writer_2'),invariant(inv8)],true),po(conc_4,'Well-definedness of action',[action(act2)],true),po(conc_4,'Invariant preservation',[event('Writer_3'),event('Writer_3'),invariant(inv2)],false),po(conc_4,'Invariant preservation',[event('Writer_3'),event('Writer_3'),invariant(inv4)],false),po(conc_4,'Invariant preservation',[event('Writer_3'),event('Writer_3'),invariant(inv5)],false),po(conc_4,'Invariant preservation',[event('Writer_3'),event('Writer_3'),invariant(inv6)],true),po(conc_4,'Invariant preservation',[event('Writer_3'),event('Writer_3'),invariant(inv7)],true),po(conc_4,'Invariant preservation',[event('Writer_3'),event('Writer_3'),invariant(inv8)],true),po(conc_4,'Well-definedness of action',[action(act2)],true),po(conc_4,'Invariant preservation',[event('Writer_41'),event('Writer_4'),invariant(inv4)],true),po(conc_4,'Invariant preservation',[event('Writer_41'),event('Writer_4'),invariant(inv5)],false),po(conc_4,'Invariant preservation',[event('Writer_41'),event('Writer_4'),invariant(inv6)],true),po(conc_4,'Invariant preservation',[event('Writer_41'),event('Writer_4'),invariant(inv7)],true),po(conc_4,'Invariant preservation',[event('Writer_41'),event('Writer_4'),invariant(inv8)],true),po(conc_4,'Guard strengthening (merge)',[event('Writer_41'),event('Writer_42'),event('Writer_4')],true),po(conc_4,'Action simulation',[event('Writer_41'),action(act2),event('Writer_4')],false),po(conc_4,'Invariant preservation',[event('Writer_51'),event('Writer_5'),invariant(inv4)],true),po(conc_4,'Invariant preservation',[event('Writer_51'),event('Writer_5'),invariant(inv5)],false),po(conc_4,'Invariant preservation',[event('Writer_51'),event('Writer_5'),invariant(inv6)],true),po(conc_4,'Invariant preservation',[event('Writer_51'),event('Writer_5'),invariant(inv7)],true),po(conc_4,'Invariant preservation',[event('Writer_51'),event('Writer_5'),invariant(inv8)],true),po(conc_4,'Guard strengthening (merge)',[event('Writer_51'),event('Writer_52'),event('Writer_5')],true),po(conc_3,'Well-definedness of Invariant',[invariant(inv2)],true),po(conc_3,'Invariant establishment',[event('INITIALISATION'),event('INITIALISATION'),invariant(inv1)],false),po(conc_3,'Invariant establishment',[event('INITIALISATION'),event('INITIALISATION'),invariant(inv2)],true),po(conc_3,'Action simulation',[event('INITIALISATION'),action(act12),event('INITIALISATION')],true),po(conc_3,'Action simulation',[event('INITIALISATION'),action(act3),event('INITIALISATION')],true),po(conc_3,'Well-definedness of action',[action(act1)],true),po(conc_3,'Action simulation',[event('Reader_3'),action(act1),event('Reader_3')],false),po(conc_3,'Invariant preservation',[event('Writer_1'),event('Writer_1'),invariant(inv1)],false),po(conc_3,'Invariant preservation',[event('Writer_1'),event('Writer_1'),invariant(inv2)],false),po(conc_3,'Well-definedness of action',[action(act5)],false),po(conc_3,'Action simulation',[event('Writer_1'),action(act2),event('Writer_1')],true),po(conc_3,'Action simulation',[event('Writer_42'),action(act2),event('Writer_42')],true),po(conc_3,'Action simulation',[event('Writer_51'),action(act2),event('Writer_51')],true),po(conc_2,'Well-definedness of Invariant',[invariant(inv8)],true),po(conc_2,'Well-definedness of Invariant',[invariant(inv9)],true),po(conc_2,'Well-definedness of Invariant',[invariant(inv10)],true),po(conc_2,'Well-definedness of Invariant',[invariant(inv13)],true),po(conc_2,'Well-definedness of Invariant',[invariant(inv14)],true),po(conc_2,'Well-definedness of Invariant',[invariant(inv17)],false),po(conc_2,'Theorem',[invariant(thm1)],false),po(conc_2,'Well-definedness of Theorem',[invariant(thm2)],false),po(conc_2,'Theorem',[invariant(thm2)],false),po(conc_2,'Invariant establishment',[event('INITIALISATION'),event('INITIALISATION'),invariant(inv1)],true),po(conc_2,'Invariant establishment',[event('INITIALISATION'),event('INITIALISATION'),invariant(inv2)],true),po(conc_2,'Invariant establishment',[event('INITIALISATION'),event('INITIALISATION'),invariant(inv3)],true),po(conc_2,'Invariant establishment',[event('INITIALISATION'),event('INITIALISATION'),invariant(inv4)],true),po(conc_2,'Invariant establishment',[event('INITIALISATION'),event('INITIALISATION'),invariant(inv5)],true),po(conc_2,'Invariant establishment',[event('INITIALISATION'),event('INITIALISATION'),invariant(inv6)],false),po(conc_2,'Invariant establishment',[event('INITIALISATION'),event('INITIALISATION'),invariant(inv7)],false),po(conc_2,'Invariant establishment',[event('INITIALISATION'),event('INITIALISATION'),invariant(inv8)],true),po(conc_2,'Invariant establishment',[event('INITIALISATION'),event('INITIALISATION'),invariant(inv9)],true),po(conc_2,'Invariant establishment',[event('INITIALISATION'),event('INITIALISATION'),invariant(inv10)],true),po(conc_2,'Invariant establishment',[event('INITIALISATION'),event('INITIALISATION'),invariant(inv11)],true),po(conc_2,'Invariant establishment',[event('INITIALISATION'),event('INITIALISATION'),invariant(inv12)],true),po(conc_2,'Invariant establishment',[event('INITIALISATION'),event('INITIALISATION'),invariant(inv13)],true),po(conc_2,'Invariant establishment',[event('INITIALISATION'),event('INITIALISATION'),invariant(inv14)],false),po(conc_2,'Invariant establishment',[event('INITIALISATION'),event('INITIALISATION'),invariant(inv15)],true),po(conc_2,'Invariant establishment',[event('INITIALISATION'),event('INITIALISATION'),invariant(inv16)],true),po(conc_2,'Invariant establishment',[event('INITIALISATION'),event('INITIALISATION'),invariant(inv17)],true),po(conc_2,'Action simulation',[event('INITIALISATION'),action(act11),event('INITIALISATION')],true),po(conc_2,'Action simulation',[event('INITIALISATION'),action(act12),event('INITIALISATION')],true),po(conc_2,'Invariant preservation',[event('Reader_1'),event('Reader_1'),invariant(inv1)],true),po(conc_2,'Invariant preservation',[event('Reader_1'),event('Reader_1'),invariant(inv8)],false),po(conc_2,'Invariant preservation',[event('Reader_1'),event('Reader_1'),invariant(inv9)],true),po(conc_2,'Invariant preservation',[event('Reader_1'),event('Reader_1'),invariant(inv12)],true),po(conc_2,'Well-definedness of witness',[witness(v)],true),po(conc_2,'Invariant preservation',[event('Reader_2'),event('Reader_2'),invariant(inv4)],true),po(conc_2,'Invariant preservation',[event('Reader_2'),event('Reader_2'),invariant(inv8)],true),po(conc_2,'Invariant preservation',[event('Reader_2'),event('Reader_2'),invariant(inv9)],true),po(conc_2,'Guard strengthening (split)',[event('Reader_2'),guard(grd2),event('Reader_2'),event('Reader_2')],true),po(conc_2,'Well-definedness of action',[action(act2)],true),po(conc_2,'Action simulation',[event('Reader_2'),action(act3),event('Reader_2')],true),po(conc_2,'Invariant preservation',[event('Reader_3'),event('Reader_3'),invariant(inv8)],true),po(conc_2,'Invariant preservation',[event('Reader_3'),event('Reader_3'),invariant(inv9)],true),po(conc_2,'Well-definedness of action',[action(act1)],true),po(conc_2,'Action simulation',[event('Reader_3'),action(act1),event('Reader_3')],true),po(conc_2,'Invariant preservation',[event('Writer_1'),event('Writer_1'),invariant(inv2)],false),po(conc_2,'Invariant preservation',[event('Writer_1'),event('Writer_1'),invariant(inv5)],false),po(conc_2,'Invariant preservation',[event('Writer_1'),event('Writer_1'),invariant(inv7)],false),po(conc_2,'Invariant preservation',[event('Writer_1'),event('Writer_1'),invariant(inv8)],true),po(conc_2,'Invariant preservation',[event('Writer_1'),event('Writer_1'),invariant(inv9)],true),po(conc_2,'Invariant preservation',[event('Writer_1'),event('Writer_1'),invariant(inv10)],false),po(conc_2,'Invariant preservation',[event('Writer_1'),event('Writer_1'),invariant(inv11)],true),po(conc_2,'Invariant preservation',[event('Writer_1'),event('Writer_1'),invariant(inv12)],true),po(conc_2,'Invariant preservation',[event('Writer_1'),event('Writer_1'),invariant(inv13)],false),po(conc_2,'Invariant preservation',[event('Writer_1'),event('Writer_1'),invariant(inv14)],true),po(conc_2,'Invariant preservation',[event('Writer_1'),event('Writer_1'),invariant(inv15)],true),po(conc_2,'Invariant preservation',[event('Writer_1'),event('Writer_1'),invariant(inv16)],true),po(conc_2,'Invariant preservation',[event('Writer_1'),event('Writer_1'),invariant(inv17)],false),po(conc_2,'Well-definedness of action',[action(act4)],true),po(conc_2,'Well-definedness of action',[action(act5)],false),po(conc_2,'Invariant preservation',[event('Writer_2'),event('Writer_2'),invariant(inv11)],true),po(conc_2,'Invariant preservation',[event('Writer_2'),event('Writer_2'),invariant(inv13)],false),po(conc_2,'Invariant preservation',[event('Writer_2'),event('Writer_2'),invariant(inv14)],true),po(conc_2,'Invariant preservation',[event('Writer_2'),event('Writer_2'),invariant(inv15)],true),po(conc_2,'Invariant preservation',[event('Writer_2'),event('Writer_2'),invariant(inv16)],true),po(conc_2,'Invariant preservation',[event('Writer_3'),event('Writer_3'),invariant(inv11)],true),po(conc_2,'Invariant preservation',[event('Writer_3'),event('Writer_3'),invariant(inv13)],false),po(conc_2,'Invariant preservation',[event('Writer_3'),event('Writer_3'),invariant(inv14)],true),po(conc_2,'Invariant preservation',[event('Writer_3'),event('Writer_3'),invariant(inv15)],true),po(conc_2,'Invariant preservation',[event('Writer_3'),event('Writer_3'),invariant(inv16)],true),po(conc_2,'Invariant preservation',[event('Writer_41'),event('Writer_41'),invariant(inv6)],false),po(conc_2,'Invariant preservation',[event('Writer_41'),event('Writer_41'),invariant(inv8)],true),po(conc_2,'Invariant preservation',[event('Writer_41'),event('Writer_41'),invariant(inv10)],true),po(conc_2,'Invariant preservation',[event('Writer_41'),event('Writer_41'),invariant(inv11)],true),po(conc_2,'Invariant preservation',[event('Writer_41'),event('Writer_41'),invariant(inv13)],true),po(conc_2,'Invariant preservation',[event('Writer_41'),event('Writer_41'),invariant(inv14)],false),po(conc_2,'Invariant preservation',[event('Writer_41'),event('Writer_41'),invariant(inv15)],true),po(conc_2,'Invariant preservation',[event('Writer_41'),event('Writer_41'),invariant(inv16)],false),po(conc_2,'Invariant preservation',[event('Writer_42'),event('Writer_42'),invariant(inv6)],false),po(conc_2,'Invariant preservation',[event('Writer_42'),event('Writer_42'),invariant(inv8)],false),po(conc_2,'Invariant preservation',[event('Writer_42'),event('Writer_42'),invariant(inv10)],false),po(conc_2,'Invariant preservation',[event('Writer_42'),event('Writer_42'),invariant(inv11)],true),po(conc_2,'Invariant preservation',[event('Writer_42'),event('Writer_42'),invariant(inv13)],true),po(conc_2,'Invariant preservation',[event('Writer_42'),event('Writer_42'),invariant(inv14)],false),po(conc_2,'Invariant preservation',[event('Writer_42'),event('Writer_42'),invariant(inv15)],false),po(conc_2,'Invariant preservation',[event('Writer_42'),event('Writer_42'),invariant(inv16)],true),po(conc_2,'Invariant preservation',[event('Writer_51'),event('Writer_51'),invariant(inv3)],true),po(conc_2,'Invariant preservation',[event('Writer_51'),event('Writer_51'),invariant(inv8)],false),po(conc_2,'Invariant preservation',[event('Writer_51'),event('Writer_51'),invariant(inv10)],false),po(conc_2,'Invariant preservation',[event('Writer_51'),event('Writer_51'),invariant(inv11)],true),po(conc_2,'Invariant preservation',[event('Writer_51'),event('Writer_51'),invariant(inv12)],true),po(conc_2,'Invariant preservation',[event('Writer_51'),event('Writer_51'),invariant(inv13)],true),po(conc_2,'Invariant preservation',[event('Writer_51'),event('Writer_51'),invariant(inv14)],false),po(conc_2,'Invariant preservation',[event('Writer_51'),event('Writer_51'),invariant(inv15)],true),po(conc_2,'Invariant preservation',[event('Writer_51'),event('Writer_51'),invariant(inv16)],true),po(conc_2,'Guard strengthening (split)',[event('Writer_51'),guard(grd2),event('Writer_51'),event('Writer_51')],false),po(conc_2,'Invariant preservation',[event('Writer_52'),event('Writer_52'),invariant(inv3)],true),po(conc_2,'Invariant preservation',[event('Writer_52'),event('Writer_52'),invariant(inv10)],true),po(conc_2,'Invariant preservation',[event('Writer_52'),event('Writer_52'),invariant(inv11)],true),po(conc_2,'Invariant preservation',[event('Writer_52'),event('Writer_52'),invariant(inv12)],true),po(conc_2,'Invariant preservation',[event('Writer_52'),event('Writer_52'),invariant(inv13)],true),po(conc_2,'Invariant preservation',[event('Writer_52'),event('Writer_52'),invariant(inv14)],false),po(conc_2,'Invariant preservation',[event('Writer_52'),event('Writer_52'),invariant(inv15)],true),po(conc_2,'Invariant preservation',[event('Writer_52'),event('Writer_52'),invariant(inv16)],true),po(conc_2,'Guard strengthening (split)',[event('Writer_52'),guard(grd2),event('Writer_52'),event('Writer_52')],true),po(conc_1,'Well-definedness of Invariant',[invariant(inv3)],false),po(conc_1,'Well-definedness of Invariant',[invariant(inv4)],false),po(conc_1,'Well-definedness of Invariant',[invariant(inv7)],false),po(conc_1,'Invariant establishment',[event('INITIALISATION'),event('INITIALISATION'),invariant(inv1)],true),po(conc_1,'Invariant establishment',[event('INITIALISATION'),event('INITIALISATION'),invariant(inv2)],true),po(conc_1,'Invariant establishment',[event('INITIALISATION'),event('INITIALISATION'),invariant(inv3)],true),po(conc_1,'Invariant establishment',[event('INITIALISATION'),event('INITIALISATION'),invariant(inv4)],true),po(conc_1,'Invariant establishment',[event('INITIALISATION'),event('INITIALISATION'),invariant(inv5)],false),po(conc_1,'Invariant establishment',[event('INITIALISATION'),event('INITIALISATION'),invariant(inv7)],true),po(conc_1,'Invariant establishment',[event('INITIALISATION'),event('INITIALISATION'),invariant(inv8)],true),po(conc_1,'Invariant establishment',[event('INITIALISATION'),event('INITIALISATION'),invariant(inv9)],false),po(conc_1,'Invariant establishment',[event('INITIALISATION'),event('INITIALISATION'),invariant(inv10)],false),po(conc_1,'Invariant establishment',[event('INITIALISATION'),event('INITIALISATION'),invariant(inv11)],true),po(conc_1,'Invariant preservation',[event('Reader_1'),invariant(inv2)],true),po(conc_1,'Invariant preservation',[event('Reader_1'),invariant(inv7)],true),po(conc_1,'Invariant preservation',[event(read),event('Reader_2'),invariant(inv2)],true),po(conc_1,'Invariant preservation',[event(read),event('Reader_2'),invariant(inv3)],true),po(conc_1,'Invariant preservation',[event(read),event('Reader_2'),invariant(inv4)],true),po(conc_1,'Invariant preservation',[event(read),event('Reader_2'),invariant(inv7)],true),po(conc_1,'Guard strengthening (split)',[event(read),guard(grd1),event(read),event('Reader_2')],false),po(conc_1,'Invariant preservation',[event('Reader_3'),invariant(inv2)],true),po(conc_1,'Invariant preservation',[event('Reader_3'),invariant(inv7)],false),po(conc_1,'Well-definedness of action',[action(act1)],false),po(conc_1,'Invariant preservation',[event('Writer_1'),invariant(inv1)],true),po(conc_1,'Invariant preservation',[event('Writer_1'),invariant(inv5)],false),po(conc_1,'Invariant preservation',[event('Writer_1'),invariant(inv8)],false),po(conc_1,'Invariant preservation',[event('Writer_1'),invariant(inv9)],true),po(conc_1,'Invariant preservation',[event('Writer_1'),invariant(inv10)],false),po(conc_1,'Invariant preservation',[event('Writer_1'),invariant(inv11)],true),po(conc_1,'Invariant preservation',[event('Writer_2'),invariant(inv1)],true),po(conc_1,'Invariant preservation',[event('Writer_2'),invariant(inv9)],true),po(conc_1,'Invariant preservation',[event('Writer_2'),invariant(inv10)],true),po(conc_1,'Invariant preservation',[event('Writer_2'),invariant(inv11)],true),po(conc_1,'Invariant preservation',[event('Writer_3'),invariant(inv1)],true),po(conc_1,'Invariant preservation',[event('Writer_3'),invariant(inv9)],true),po(conc_1,'Invariant preservation',[event('Writer_3'),invariant(inv10)],true),po(conc_1,'Invariant preservation',[event('Writer_3'),invariant(inv11)],true),po(conc_1,'Invariant preservation',[event('Writer_41'),invariant(inv1)],true),po(conc_1,'Invariant preservation',[event('Writer_41'),invariant(inv9)],true),po(conc_1,'Invariant preservation',[event('Writer_41'),invariant(inv10)],true),po(conc_1,'Invariant preservation',[event('Writer_41'),invariant(inv11)],false),po(conc_1,'Well-definedness of witness',[witness(d)],false),po(conc_1,'Invariant preservation',[event(write),event('Writer_42'),invariant(inv1)],true),po(conc_1,'Invariant preservation',[event(write),event('Writer_42'),invariant(inv8)],false),po(conc_1,'Invariant preservation',[event(write),event('Writer_42'),invariant(inv9)],true),po(conc_1,'Invariant preservation',[event(write),event('Writer_42'),invariant(inv10)],false),po(conc_1,'Invariant preservation',[event(write),event('Writer_42'),invariant(inv11)],false),po(conc_1,'Well-definedness of witness',[witness(d)],false),po(conc_1,'Invariant preservation',[event(write),event('Writer_51'),invariant(inv1)],true),po(conc_1,'Invariant preservation',[event(write),event('Writer_51'),invariant(inv8)],false),po(conc_1,'Invariant preservation',[event(write),event('Writer_51'),invariant(inv9)],true),po(conc_1,'Invariant preservation',[event(write),event('Writer_51'),invariant(inv10)],false),po(conc_1,'Invariant preservation',[event(write),event('Writer_51'),invariant(inv11)],true),po(conc_1,'Invariant preservation',[event('Writer_52'),invariant(inv1)],true),po(conc_1,'Invariant preservation',[event('Writer_52'),invariant(inv9)],true),po(conc_1,'Invariant preservation',[event('Writer_52'),invariant(inv10)],false),po(conc_1,'Invariant preservation',[event('Writer_52'),invariant(inv11)],true),po(conc_0,'Well-definedness of Invariant',[invariant(inv8)],true),po(conc_0,'Well-definedness of Invariant',[invariant(inv9)],false),po(conc_0,'Invariant establishment',[event('INITIALISATION'),invariant(inv1)],true),po(conc_0,'Invariant establishment',[event('INITIALISATION'),invariant(inv2)],true),po(conc_0,'Invariant establishment',[event('INITIALISATION'),invariant(inv3)],false),po(conc_0,'Invariant establishment',[event('INITIALISATION'),invariant(inv4)],false),po(conc_0,'Invariant establishment',[event('INITIALISATION'),invariant(inv5)],false),po(conc_0,'Invariant establishment',[event('INITIALISATION'),invariant(inv6)],false),po(conc_0,'Invariant establishment',[event('INITIALISATION'),invariant(inv7)],false),po(conc_0,'Invariant establishment',[event('INITIALISATION'),invariant(inv8)],true),po(conc_0,'Invariant establishment',[event('INITIALISATION'),invariant(inv9)],true),po(conc_0,'Invariant preservation',[event(write),invariant(inv1)],false),po(conc_0,'Invariant preservation',[event(write),invariant(inv3)],false),po(conc_0,'Invariant preservation',[event(write),invariant(inv5)],false),po(conc_0,'Invariant preservation',[event(write),invariant(inv6)],false),po(conc_0,'Invariant preservation',[event(write),invariant(inv7)],false),po(conc_0,'Well-definedness of Guard',[guard(grd1),event(read)],false),po(conc_0,'Invariant preservation',[event(read),invariant(inv2)],false),po(conc_0,'Invariant preservation',[event(read),invariant(inv4)],false),po(conc_0,'Invariant preservation',[event(read),invariant(inv5)],false),po(conc_0,'Invariant preservation',[event(read),invariant(inv6)],false),po(conc_0,'Invariant preservation',[event(read),invariant(inv7)],false),po(conc_0,'Invariant preservation',[event(read),invariant(inv8)],false),po(conc_0,'Invariant preservation',[event(read),invariant(inv9)],false),po(conc_0,'Well-definedness of action',[action(act4)],false)],_Error)).
2