1		package(load_event_b_project([event_b_model(none,'Guard0_simerror',[sees(none,[]),refines(none,'Guard0'),variables(none,[identifier(none,y)]),invariant(none,[equal(rodinpos('Guard0_simerror',invy,'_x33MhOSREeaU86Rx_hNGRg'),identifier(none,y),add(none,identifier(none,x),integer(none,1)))]),theorems(none,[]),events(none,[event(rodinpos('Guard0_simerror','INITIALISATION','_j0sMseSREeaU86Rx_hNGRh'),'INITIALISATION',ordinary(none),['INITIALISATION'],[],[],[],[assign(rodinpos('Guard0_simerror',iniy,'_x32lcOSREeaU86Rx_hNGRg'),[identifier(none,y)],[integer(none,21)])],[]),event(rodinpos('Guard0_simerror',even_dec,'_j0sMseSREeaU86Rx_hNGRi'),even_dec,ordinary(none),[even_dec],[],[conjunct(rodinpos('Guard0_simerror',g,'_x33MgOSREeaU86Rx_hNGRg'),greater(none,identifier(none,y),integer(none,1)),equal(none,modulo(none,identifier(none,y),integer(none,2)),integer(none,1)))],[],[assign(rodinpos('Guard0_simerror',dec,'_x33MgeSREeaU86Rx_hNGRg'),[identifier(none,y)],[minus(none,identifier(none,y),integer(none,1))])],[witness(none,identifier(none,p),equal(rodinpos('Guard0_simerror',p,'_UBMCQOSSEeaU86Rx_hNGRg'),identifier(none,p),integer(none,21)))]),event(rodinpos('Guard0_simerror',odd_dec,'_j0sMseSREeaU86Rx_hNGRj'),odd_dec,ordinary(none),[odd_dec],[],[equal(rodinpos('Guard0_simerror',g,'_x33MguSREeaU86Rx_hNGRg'),modulo(none,identifier(none,y),integer(none,2)),integer(none,0))],[],[assign(rodinpos('Guard0_simerror',dec,'_x33Mg-SREeaU86Rx_hNGRg'),[identifier(none,y)],[minus(none,identifier(none,y),integer(none,1))])],[])])]),event_b_model(none,'Guard0',[sees(none,[]),variables(none,[identifier(none,x)]),invariant(none,[member(rodinpos('Guard0',inv,'_j0sMsuSREeaU86Rx_hNGRg'),identifier(none,x),natural_set(none))]),theorems(none,[]),events(none,[event(rodinpos('Guard0','INITIALISATION','\''),'INITIALISATION',ordinary(none),[],[],[],[],[assign(rodinpos('Guard0',ini,'_j0sMsOSREeaU86Rx_hNGRg'),[identifier(none,x)],[integer(none,20)])],[]),event(rodinpos('Guard0',even_dec,'_j0sMs-SREeaU86Rx_hNGRg'),even_dec,ordinary(none),[],[identifier(rodinpos('Guard0',[],'_DgAH4OSSEeaU86Rx_hNGRg'),p)],[conjunct(rodinpos('Guard0',g1,'_j0sMtOSREeaU86Rx_hNGRg'),greater_equal(none,minus(none,identifier(none,x),identifier(none,p)),integer(none,0)),greater(none,identifier(none,p),integer(none,0))),conjunct(rodinpos('Guard0',g,'_j0szweSREeaU86Rx_hNGRg'),greater(none,identifier(none,x),integer(none,0)),equal(none,modulo(none,identifier(none,x),integer(none,2)),integer(none,0)))],[],[assign(rodinpos('Guard0',dec,'_j0sMteSREeaU86Rx_hNGRg'),[identifier(none,x)],[minus(none,identifier(none,x),identifier(none,p))])],[]),event(rodinpos('Guard0',odd_dec,'_j0szwOSREeaU86Rx_hNGRg'),odd_dec,ordinary(none),[],[],[equal(rodinpos('Guard0',g,'_DgAH4eSSEeaU86Rx_hNGRg'),modulo(none,identifier(none,x),integer(none,2)),integer(none,1))],[],[assign(rodinpos('Guard0',dec,'_j0szwuSREeaU86Rx_hNGRg'),[identifier(none,x)],[minus(none,identifier(none,x),integer(none,1))])],[])])])],[],[exporter_version(3),po('Guard0_simerror','Invariant establishment',[event('INITIALISATION'),event('INITIALISATION'),invariant(invy)],true),po('Guard0_simerror','Well-definedness of Guard',[guard(g),event(even_dec)],true),po('Guard0_simerror','Invariant preservation',[event(even_dec),event(even_dec),invariant(invy)],false),po('Guard0_simerror','Guard strengthening (split)',[event(even_dec),guard(g1),event(even_dec),event(even_dec)],false),po('Guard0_simerror','Guard strengthening (split)',[event(even_dec),guard(g),event(even_dec),event(even_dec)],false),po('Guard0_simerror','Well-definedness of Guard',[guard(g),event(odd_dec)],true),po('Guard0_simerror','Invariant preservation',[event(odd_dec),event(odd_dec),invariant(invy)],false),po('Guard0_simerror','Guard strengthening (split)',[event(odd_dec),guard(g),event(odd_dec),event(odd_dec)],false),po('Guard0','Invariant establishment',[event('INITIALISATION'),invariant(inv)],true),po('Guard0','Well-definedness of Guard',[guard(g),event(even_dec)],true),po('Guard0','Invariant preservation',[event(even_dec),invariant(inv)],false),po('Guard0','Well-definedness of Guard',[guard(g),event(odd_dec)],true),po('Guard0','Invariant preservation',[event(odd_dec),invariant(inv)],true)],_Error)).
2