1		package(load_event_b_project([event_b_model(none,m1_c2,[sees(none,[c1_2]),variables(none,[identifier(none,abal),identifier(none,lost),identifier(none,purse)]),invariant(none,[subset(rodinpos(inv1,'_9I_JMVohEeGfE_H3Zsi4bQ'),identifier(none,purse),identifier(none,'PURSE')),member(rodinpos(inv2,'_9I_JMlohEeGfE_H3Zsi4bQ'),identifier(none,abal),total_function(none,identifier(none,purse),natural_set(none))),member(rodinpos(inv3,'_9I_JM1ohEeGfE_H3Zsi4bQ'),identifier(none,lost),total_function(none,identifier(none,purse),natural_set(none)))]),theorems(none,[]),events(none,[event(rodinpos('INITIALISATION','\''),'INITIALISATION',ordinary(none),[],[],[],[],[assign(rodinpos(act1,'_9I_wQFohEeGfE_H3Zsi4bQ'),[identifier(none,purse)],[empty_set(none)]),assign(rodinpos(act2,'_9I_wQVohEeGfE_H3Zsi4bQ'),[identifier(none,abal)],[empty_set(none)]),assign(rodinpos(act3,'_9I_wQlohEeGfE_H3Zsi4bQ'),[identifier(none,lost)],[empty_set(none)])],[]),event(rodinpos(createPurse,'_9I_wQ1ohEeGfE_H3Zsi4bQ'),createPurse,ordinary(none),[],[identifier(rodinpos([],'_9I_wRVohEeGfE_H3Zsi4bQ'),a),identifier(rodinpos([],'_9I_wRFohEeGfE_H3Zsi4bQ'),p)],[member(rodinpos(grd1,'_9JAXUFohEeGfE_H3Zsi4bQ'),identifier(none,p),set_subtraction(none,identifier(none,'PURSE'),identifier(none,purse))),conjunct(rodinpos(grd2,'_9JAXUVohEeGfE_H3Zsi4bQ'),member(none,identifier(none,a),natural_set(none)),less_equal(none,identifier(none,a),identifier(none,lim))),greater(rodinpos(grd3,'_9JAXUlohEeGfE_H3Zsi4bQ'),identifier(none,a),integer(none,0))],[],[assign(rodinpos(act1,'_9JAXU1ohEeGfE_H3Zsi4bQ'),[identifier(none,purse)],[union(none,identifier(none,purse),set_extension(none,[identifier(none,p)]))]),assign(rodinpos(act2,'_9JA-YFohEeGfE_H3Zsi4bQ'),[identifier(none,abal)],[overwrite(none,identifier(none,abal),set_extension(none,[couple(none,[identifier(none,p),identifier(none,a)])]))]),assign(rodinpos(act3,'_9JA-YVohEeGfE_H3Zsi4bQ'),[identifier(none,lost)],[overwrite(none,identifier(none,lost),set_extension(none,[couple(none,[identifier(none,p),integer(none,0)])]))])],[]),event(rodinpos('TransferOk','_9JA-YlohEeGfE_H3Zsi4bQ'),'TransferOk',ordinary(none),[],[identifier(rodinpos([],'_9JA-ZVohEeGfE_H3Zsi4bQ'),a),identifier(rodinpos([],'_9JA-Y1ohEeGfE_H3Zsi4bQ'),p1),identifier(rodinpos([],'_9JA-ZFohEeGfE_H3Zsi4bQ'),p2)],[member(rodinpos(grd1,'_9JA-ZlohEeGfE_H3Zsi4bQ'),identifier(none,p1),identifier(none,purse)),member(rodinpos(grd2,'_9JBlcFohEeGfE_H3Zsi4bQ'),identifier(none,p2),identifier(none,purse)),not_equal(rodinpos(grd3,'_9JBlcVohEeGfE_H3Zsi4bQ'),identifier(none,p1),identifier(none,p2)),member(rodinpos(grd4,'_9JBlclohEeGfE_H3Zsi4bQ'),identifier(none,a),natural_set(none)),greater_equal(rodinpos(grd6,'_9JBlc1ohEeGfE_H3Zsi4bQ'),function(none,identifier(none,abal),[identifier(none,p1)]),identifier(none,a))],[],[assign(rodinpos(act1,'_9JCMgFohEeGfE_H3Zsi4bQ'),[identifier(none,abal)],[overwrite(none,overwrite(none,identifier(none,abal),set_extension(none,[couple(none,[identifier(none,p1),minus(none,function(none,identifier(none,abal),[identifier(none,p1)]),identifier(none,a))])])),set_extension(none,[couple(none,[identifier(none,p2),add(none,function(none,identifier(none,abal),[identifier(none,p2)]),identifier(none,a))])]))])],[]),event(rodinpos('TransferFail','_9JCMgVohEeGfE_H3Zsi4bQ'),'TransferFail',ordinary(none),[],[identifier(rodinpos([],'_9JCMg1ohEeGfE_H3Zsi4bQ'),a),identifier(rodinpos([],'_9JCMglohEeGfE_H3Zsi4bQ'),p1)],[member(rodinpos(grd1,'_9JCMhFohEeGfE_H3Zsi4bQ'),identifier(none,p1),identifier(none,purse)),member(rodinpos(grd2,'_9JCzkFohEeGfE_H3Zsi4bQ'),identifier(none,a),natural_set(none)),greater_equal(rodinpos(grd4,'_9JCzkVohEeGfE_H3Zsi4bQ'),function(none,identifier(none,abal),[identifier(none,p1)]),identifier(none,a))],[],[assign(rodinpos(act1,'_9JCzklohEeGfE_H3Zsi4bQ'),[identifier(none,abal)],[overwrite(none,identifier(none,abal),set_extension(none,[couple(none,[identifier(none,p1),minus(none,function(none,identifier(none,abal),[identifier(none,p1)]),identifier(none,a))])]))]),assign(rodinpos(act2,'_9JCzk1ohEeGfE_H3Zsi4bQ'),[identifier(none,lost)],[overwrite(none,identifier(none,lost),set_extension(none,[couple(none,[identifier(none,p1),add(none,function(none,identifier(none,lost),[identifier(none,p1)]),identifier(none,a))])]))])],[]),event(rodinpos('Recover','_9JCzlFohEeGfE_H3Zsi4bQ'),'Recover',ordinary(none),[],[identifier(rodinpos([],'_9JDaoVohEeGfE_H3Zsi4bQ'),a),identifier(rodinpos([],'_9JDaoFohEeGfE_H3Zsi4bQ'),p1)],[member(rodinpos(grd1,'_9JDaolohEeGfE_H3Zsi4bQ'),identifier(none,p1),identifier(none,purse)),member(rodinpos(grd2,'_9JDao1ohEeGfE_H3Zsi4bQ'),identifier(none,a),natural_set(none)),greater_equal(rodinpos(grd4,'_9JDapFohEeGfE_H3Zsi4bQ'),function(none,identifier(none,lost),[identifier(none,p1)]),identifier(none,a))],[],[assign(rodinpos(act2,'_9JDapVohEeGfE_H3Zsi4bQ'),[identifier(none,lost)],[overwrite(none,identifier(none,lost),set_extension(none,[couple(none,[identifier(none,p1),minus(none,function(none,identifier(none,lost),[identifier(none,p1)]),identifier(none,a))])]))]),assign(rodinpos(act1,'_9JDaplohEeGfE_H3Zsi4bQ'),[identifier(none,abal)],[overwrite(none,identifier(none,abal),set_extension(none,[couple(none,[identifier(none,p1),add(none,function(none,identifier(none,abal),[identifier(none,p1)]),identifier(none,a))])]))])],[])])])],[event_b_context(none,c1_2,[extends(none,[]),constants(none,[identifier(none,'PURSE1'),identifier(none,'PURSE2'),identifier(none,lim)]),axioms(none,[equal(rodinpos(cons1,'_VF8RlFoiEeGfE_H3Zsi4bQ'),identifier(none,'PURSE'),set_extension(none,[identifier(none,'PURSE1'),identifier(none,'PURSE2')])),not_equal(rodinpos(cons3,'_VF84oFoiEeGfE_H3Zsi4bQ'),identifier(none,'PURSE1'),identifier(none,'PURSE2')),not_equal(rodinpos(cons3b,'_VF84oVoiEeGfE_H3Zsi4bQ'),identifier(none,'PURSE2'),identifier(none,'PURSE1')),negation(rodinpos(cons3c,'_VF84oloiEeGfE_H3Zsi4bQ'),equal(none,identifier(none,'PURSE1'),identifier(none,'PURSE2'))),equal(rodinpos(limit,'_VF84o1oiEeGfE_H3Zsi4bQ'),identifier(none,lim),integer(none,4))]),theorems(none,[]),sets(none,[deferred_set(none,'PURSE')])])],[discharged(m1_c2,'INITIALISATION',inv2),discharged(m1_c2,'INITIALISATION',inv3),discharged(m1_c2,createPurse,inv2),discharged(m1_c2,createPurse,inv3),discharged(m1_c2,'TransferOk',inv2),discharged(m1_c2,'TransferFail',inv2),discharged(m1_c2,'TransferFail',inv3),discharged(m1_c2,'Recover',inv2),discharged(m1_c2,'Recover',inv3)],_Error)).
2