1		package(load_event_b_project([event_b_model(none,'MTool1',[sees(none,['CTool0','CTool1']),refines(none,'MTool0'),variables(none,[identifier(none,phmn),identifier(none,phmn_class),identifier(none,phmn_unclassified),identifier(none,to_check)]),invariant(none,[subset(rodinpos('MTool1',inv2,'_uQkycKzXEeKAyc97jvPppg'),identifier(none,phmn),identifier(none,'Ph')),member(rodinpos('MTool1',inv3,'_uQkycazXEeKAyc97jvPppg'),identifier(none,phmn_class),partial_function(none,identifier(none,phmn),identifier(none,'PhC'))),subset(rodinpos('MTool1',inv4,'_4y1kgKtcEeK3CKTKi4LyHw'),identifier(none,phmn_unclassified),identifier(none,'Ph')),implication(rodinpos('MTool1',inv5,'_h_X30Me4EeKkMclOpYK1wA'),not_member(none,identifier(none,'C1'),identifier(none,to_check)),equal(none,identifier(none,phmn_unclassified),set_subtraction(none,identifier(none,phmn),domain(none,identifier(none,phmn_class)))))]),theorems(none,[]),events(none,[event(rodinpos('MTool1','INITIALISATION','_1c7QEatFEeKTkIXlmzbpux'),'INITIALISATION',ordinary(none),['INITIALISATION'],[],[],[],[assign(rodinpos('MTool1',act1,'_0ScrwcemEeKcxLgF3jk7CQ'),[identifier(none,to_check)],[empty_set(none)]),assign(rodinpos('MTool1',act2,'_werBsKzXEeKAyc97jvPppg'),[identifier(none,phmn)],[empty_set(none)]),assign(rodinpos('MTool1',act3,'_DJVyEKzNEeKr7oc6R_b82w'),[identifier(none,phmn_class)],[empty_set(none)]),assign(rodinpos('MTool1',act4,'_werBsazXEeKAyc97jvPppg'),[identifier(none,phmn_unclassified)],[empty_set(none)])],[]),event(rodinpos('MTool1',env_chg,'_-8nAAce0EeKkMclOpYK1wA'),env_chg,ordinary(none),[env_chg],[],[],[],[becomes_element_of(rodinpos('MTool1',act1,'_ZyHLMMenEeKcxLgF3jk7CQ'),[identifier(none,to_check)],pow_subset(none,identifier(none,'CR')))],[]),event(rodinpos('MTool1',env_chg_phmn,'_SALwALxvEeKcAbuxArixzg'),env_chg_phmn,ordinary(none),[env_chg],[identifier(rodinpos('MTool1',[],'_SALwAbxvEeKcAbuxArixzg'),'P'),identifier(rodinpos('MTool1',[],'_TX6GALxxEeKcAbuxArixzg'),p)],[not_equal(rodinpos('MTool1',grd1,'_TX6GAbxxEeKcAbuxArixzg'),identifier(none,'P'),identifier(none,phmn)),equal(rodinpos('MTool1',grd2,'_SALwArxvEeKcAbuxArixzg'),set_subtraction(none,identifier(none,'P'),set_extension(none,[identifier(none,p)])),set_subtraction(none,identifier(none,phmn),set_extension(none,[identifier(none,p)])))],[],[assign(rodinpos('MTool1',act2,'_SAMXELxvEeKcAbuxArixzg'),[identifier(none,phmn)],[identifier(none,'P')]),assign(rodinpos('MTool1',act3,'_jspN4LxzEeKcAbuxArixzg'),[identifier(none,phmn_class)],[domain_subtraction(none,set_extension(none,[identifier(none,p)]),identifier(none,phmn_class))]),assign(rodinpos('MTool1',act4,'_Eq5XoLx0EeKcAbuxArixzg'),[identifier(none,to_check)],[union(none,identifier(none,to_check),image(none,reverse(none,identifier(none,check)),set_extension(none,[identifier(none,phe)])))])],[]),event(rodinpos('MTool1',env_classify_phmn,'_3TxXwLxuEeKcAbuxArixzg'),env_classify_phmn,ordinary(none),[env_chg],[identifier(rodinpos('MTool1',[],'_3Tyl4LxuEeKcAbuxArixzg'),c),identifier(rodinpos('MTool1',[],'_3Tx-0bxuEeKcAbuxArixzg'),p)],[member(rodinpos('MTool1',grd2,'_3Tyl4bxuEeKcAbuxArixzg'),identifier(none,p),identifier(none,phmn)),member(rodinpos('MTool1',grd3,'_3TzM8LxuEeKcAbuxArixzg'),identifier(none,c),identifier(none,'PhC'))],[],[assign(rodinpos('MTool1',act2,'_3Tz0ALxuEeKcAbuxArixzg'),[identifier(none,phmn_class)],[overwrite(none,identifier(none,phmn_class),set_extension(none,[couple(none,[identifier(none,p),identifier(none,c)])]))]),assign(rodinpos('MTool1',act4,'_JNZScLx0EeKcAbuxArixzg'),[identifier(none,to_check)],[union(none,identifier(none,to_check),image(none,reverse(none,identifier(none,check)),set_extension(none,[identifier(none,phe)])))])],[]),event(rodinpos('MTool1',chk_rules,'_-8nnEMe0EeKkMclOpYK1wA'),chk_rules,ordinary(none),[chk_rules],[],[not_equal(rodinpos('MTool1',grd1,'_Geb24MeuEeKcxLgF3jk7CQ'),identifier(none,to_check),empty_set(none))],[],[becomes_element_of(rodinpos('MTool1',act1,'_KeuEMseoEeKcxLgF3jk7CQ'),[identifier(none,to_check)],pow_subset(none,identifier(none,'CR')))],[]),event(rodinpos('MTool1',chk_phmn_unclassified,'_3T0bELxuEeKcAbuxArixzg'),chk_phmn_unclassified,ordinary(none),[chk_rules],[identifier(rodinpos('MTool1',[],'_3T1CILxuEeKcAbuxArixzg'),'P')],[member(rodinpos('MTool1',grd1,'_ZJOjEMejEeKzvdpSfnFuAA'),identifier(none,'C1'),identifier(none,to_check)),equal(rodinpos('MTool1',grd2,'_EbErgcIdEeKYm6D5zmSD1A'),identifier(none,'P'),set_subtraction(none,identifier(none,phmn),domain(none,identifier(none,phmn_class))))],[],[assign(rodinpos('MTool1',act1,'_3T2QQLxuEeKcAbuxArixzg'),[identifier(none,phmn_unclassified)],[identifier(none,'P')]),assign(rodinpos('MTool1',act2,'_0vwPoMeiEeKzvdpSfnFuAA'),[identifier(none,to_check)],[set_subtraction(none,identifier(none,to_check),set_extension(none,[identifier(none,'C1')]))])],[])])]),event_b_model(none,'MTool0',[sees(none,['CTool0']),variables(none,[identifier(none,to_check)]),invariant(none,[subset(rodinpos('MTool0',inv1,'_eiRkAMemEeKcxLgF3jk7CQ'),identifier(none,to_check),identifier(none,'CR'))]),theorems(none,[]),events(none,[event(rodinpos('MTool0','INITIALISATION','\''),'INITIALISATION',ordinary(none),[],[],[],[],[assign(rodinpos('MTool0',act1,'_0ScrwcemEeKcxLgF3jk7CQ'),[identifier(none,to_check)],[empty_set(none)])],[]),event(rodinpos('MTool0',env_chg,'_NQcaYMenEeKcxLgF3jk7CQ'),env_chg,ordinary(none),[],[],[],[],[becomes_element_of(rodinpos('MTool0',act1,'_ZyHLMMenEeKcxLgF3jk7CQ'),[identifier(none,to_check)],pow_subset(none,identifier(none,'CR')))],[]),event(rodinpos('MTool0',chk_rules,'_KeuEMceoEeKcxLgF3jk7CQ'),chk_rules,ordinary(none),[],[],[not_equal(rodinpos('MTool0',grd1,'_Geb24MeuEeKcxLgF3jk7CQ'),identifier(none,to_check),empty_set(none))],[],[becomes_element_of(rodinpos('MTool0',act1,'_KeuEMseoEeKcxLgF3jk7CQ'),[identifier(none,to_check)],pow_subset(none,identifier(none,'CR')))],[])])])],[event_b_context(none,'CTool0',[extends(none,[]),constants(none,[identifier(none,'C1'),identifier(none,'C10'),identifier(none,'C11'),identifier(none,'C2'),identifier(none,'C3'),identifier(none,'C4'),identifier(none,'C5'),identifier(none,'C6'),identifier(none,'C7'),identifier(none,'C8'),identifier(none,'C9'),identifier(none,art),identifier(none,check),identifier(none,jus),identifier(none,phe),identifier(none,rea),identifier(none,use)]),abstract_constants(none,[]),axioms(none,[partition(rodinpos('CTool0',axm1,'_KJl0oMebEeK7jv5XZ4TxWg'),identifier(none,'CR'),[set_extension(none,[identifier(none,'C1')]),set_extension(none,[identifier(none,'C2')]),set_extension(none,[identifier(none,'C3')]),set_extension(none,[identifier(none,'C4')]),set_extension(none,[identifier(none,'C5')]),set_extension(none,[identifier(none,'C6')]),set_extension(none,[identifier(none,'C7')]),set_extension(none,[identifier(none,'C8')]),set_extension(none,[identifier(none,'C9')]),set_extension(none,[identifier(none,'C10')]),set_extension(none,[identifier(none,'C11')])]),partition(rodinpos('CTool0',axm2,'_mpw3IbMvEeKzEvl1Dwhbmg'),identifier(none,'E'),[set_extension(none,[identifier(none,phe)]),set_extension(none,[identifier(none,art)]),set_extension(none,[identifier(none,use)]),set_extension(none,[identifier(none,jus)]),set_extension(none,[identifier(none,rea)])]),member(rodinpos('CTool0',axm4,'_oQF4scecEeK7jv5XZ4TxWg'),identifier(none,check),relations(none,identifier(none,'CR'),identifier(none,'E'))),equal(rodinpos('CTool0',axm5,'_oQF4ssecEeK7jv5XZ4TxWg'),identifier(none,check),set_extension(none,[couple(none,[identifier(none,'C1'),identifier(none,phe)]),couple(none,[identifier(none,'C2'),identifier(none,art)]),couple(none,[identifier(none,'C3'),identifier(none,art)]),couple(none,[identifier(none,'C3'),identifier(none,phe)]),couple(none,[identifier(none,'C3'),identifier(none,use)]),couple(none,[identifier(none,'C4'),identifier(none,art)]),couple(none,[identifier(none,'C4'),identifier(none,phe)]),couple(none,[identifier(none,'C4'),identifier(none,use)]),couple(none,[identifier(none,'C5'),identifier(none,art)]),couple(none,[identifier(none,'C5'),identifier(none,phe)]),couple(none,[identifier(none,'C5'),identifier(none,use)]),couple(none,[identifier(none,'C6'),identifier(none,art)]),couple(none,[identifier(none,'C6'),identifier(none,phe)]),couple(none,[identifier(none,'C6'),identifier(none,use)]),couple(none,[identifier(none,'C7'),identifier(none,art)]),couple(none,[identifier(none,'C7'),identifier(none,phe)]),couple(none,[identifier(none,'C7'),identifier(none,use)]),couple(none,[identifier(none,'C8'),identifier(none,art)]),couple(none,[identifier(none,'C8'),identifier(none,jus)]),couple(none,[identifier(none,'C8'),identifier(none,rea)]),couple(none,[identifier(none,'C9'),identifier(none,art)]),couple(none,[identifier(none,'C9'),identifier(none,jus)]),couple(none,[identifier(none,'C9'),identifier(none,rea)]),couple(none,[identifier(none,'C10'),identifier(none,art)]),couple(none,[identifier(none,'C10'),identifier(none,jus)]),couple(none,[identifier(none,'C10'),identifier(none,rea)]),couple(none,[identifier(none,'C11'),identifier(none,art)]),couple(none,[identifier(none,'C11'),identifier(none,jus)]),couple(none,[identifier(none,'C11'),identifier(none,rea)])]))]),theorems(none,[]),sets(none,[deferred_set(none,'CR'),deferred_set(none,'E')])]),event_b_context(none,'CTool1',[extends(none,['CTool0']),constants(none,[identifier(none,eh),identifier(none,ev),identifier(none,sh),identifier(none,sv)]),abstract_constants(none,[]),axioms(none,[partition(rodinpos('CTool1',axm3,'_qRztRMemEeKcxLgF3jk7CQ'),identifier(none,'PhC'),[set_extension(none,[identifier(none,ev)]),set_extension(none,[identifier(none,eh)]),set_extension(none,[identifier(none,sv)]),set_extension(none,[identifier(none,sh)])])]),theorems(none,[]),sets(none,[deferred_set(none,'Ph'),deferred_set(none,'PhC')])])],[exporter_version(3),po('MTool1','Invariant establishment',[event('INITIALISATION'),event('INITIALISATION'),invariant(inv3)],true),po('MTool1','Invariant establishment',[event('INITIALISATION'),event('INITIALISATION'),invariant(inv5)],true),po('MTool1','Invariant preservation',[event(env_chg),event(env_chg),invariant(inv5)],false),po('MTool1','Invariant preservation',[event(env_chg),event(env_chg_phmn),invariant(inv3)],false),po('MTool1','Invariant preservation',[event(env_chg),event(env_chg_phmn),invariant(inv5)],false),po('MTool1','Invariant preservation',[event(env_chg),event(env_classify_phmn),invariant(inv3)],false),po('MTool1','Invariant preservation',[event(env_chg),event(env_classify_phmn),invariant(inv5)],false),po('MTool1','Invariant preservation',[event(chk_rules),event(chk_rules),invariant(inv5)],false),po('MTool1','Invariant preservation',[event(chk_rules),event(chk_phmn_unclassified),invariant(inv5)],true),po('MTool1','Guard strengthening (split)',[event(chk_rules),guard(grd1),event(chk_rules),event(chk_phmn_unclassified)],false),po('MTool0','Feasibility of action',[action(act1)],true),po('MTool0','Feasibility of action',[action(act1)],true)],_Error)).
2