1		package(load_event_b_project([event_b_model(none,auth_2,[sees(none,[auth_ctx1,auth_ctx2]),refines(none,auth_1),variables(none,[identifier(none,log),identifier(none,sit),identifier(none,valid)]),invariant(none,[member(rodinpos(auth_2,inv1,'1'),identifier(none,log),relations(none,identifier(none,'B'),identifier(none,'P'))),forall(rodinpos(auth_2,inv2,'2'),[identifier(none,p),identifier(none,b)],implication(none,conjunct(none,member(none,identifier(none,p),identifier(none,'P')),conjunct(none,member(none,identifier(none,b),identifier(none,'B')),conjunct(none,member(none,identifier(none,p),identifier(none,'P')),member(none,identifier(none,b),identifier(none,'B'))))),equivalence(none,member(none,couple(none,[identifier(none,p),identifier(none,b)]),identifier(none,sit)),member(none,couple(none,[identifier(none,b),identifier(none,p)]),identifier(none,log)))))]),theorems(none,[]),events(none,[event(rodinpos(auth_2,'INITIALISATION','-'),'INITIALISATION',ordinary(none),['INITIALISATION'],[],[],[],[assign(rodinpos(auth_2,act1,internal1),[identifier(none,sit)],[cartesian_product(none,identifier(none,'P'),set_extension(none,[identifier(none,nowhere)]))]),assign(rodinpos(auth_2,act2,'\''),[identifier(none,valid)],[cartesian_product(none,identifier(none,'P'),set_extension(none,[identifier(none,nowhere)]))]),assign(rodinpos(auth_2,act3,'\''),[identifier(none,log)],[cartesian_product(none,set_extension(none,[identifier(none,nowhere)]),identifier(none,'P'))])],[]),event(rodinpos(auth_2,leave,'.'),leave,ordinary(none),[pass],[identifier(rodinpos(auth_2,[],internal2),b),identifier(rodinpos(auth_2,[],'\''),p)],[member(rodinpos(auth_2,grd1,internal1),identifier(none,p),identifier(none,'P')),member(rodinpos(auth_2,grd2,internal3),identifier(none,b),identifier(none,'B')),equal(rodinpos(auth_2,grd3,internal4),function(none,identifier(none,sit),[identifier(none,p)]),identifier(none,b))],[],[assign(rodinpos(auth_2,act1,internal1),[identifier(none,sit)],[overwrite(none,identifier(none,sit),set_extension(none,[couple(none,[identifier(none,p),identifier(none,nowhere)])]))]),assign(rodinpos(auth_2,act2,'+'),[identifier(none,valid)],[overwrite(none,identifier(none,valid),set_extension(none,[couple(none,[identifier(none,p),identifier(none,nowhere)])]))]),assign(rodinpos(auth_2,act3,internal5),[identifier(none,log)],[union(none,set_subtraction(none,identifier(none,log),set_extension(none,[couple(none,[identifier(none,b),identifier(none,p)])])),set_extension(none,[couple(none,[identifier(none,nowhere),identifier(none,p)])]))])],[]),event(rodinpos(auth_2,check,'/'),check,ordinary(none),[check],[identifier(rodinpos(auth_2,[],'('),b),identifier(rodinpos(auth_2,[],'\''),p)],[member(rodinpos(auth_2,grd1,')'),identifier(none,p),identifier(none,'P')),member(rodinpos(auth_2,grd2,'*'),identifier(none,b),identifier(none,'B')),member(rodinpos(auth_2,grd3,'+'),couple(none,[identifier(none,p),identifier(none,b)]),identifier(none,aut))],[],[assign(rodinpos(auth_2,act1,','),[identifier(none,valid)],[overwrite(none,identifier(none,valid),set_extension(none,[couple(none,[identifier(none,p),identifier(none,b)])]))])],[])])]),event_b_model(none,auth_1,[sees(none,[auth_ctx1,auth_ctx2]),refines(none,auth_0),variables(none,[identifier(none,sit),identifier(none,valid)]),invariant(none,[subset(rodinpos(auth_1,inv1,'-'),identifier(none,valid),identifier(none,aut)),member(rodinpos(auth_1,inv2,'.'),identifier(none,valid),total_function(none,identifier(none,'P'),identifier(none,'B')))]),theorems(none,[]),events(none,[event(rodinpos(auth_1,'INITIALISATION','*'),'INITIALISATION',ordinary(none),['INITIALISATION'],[],[],[],[assign(rodinpos(auth_1,act1,internal1),[identifier(none,sit)],[cartesian_product(none,identifier(none,'P'),set_extension(none,[identifier(none,nowhere)]))]),assign(rodinpos(auth_1,act2,'\''),[identifier(none,valid)],[cartesian_product(none,identifier(none,'P'),set_extension(none,[identifier(none,nowhere)]))])],[]),event(rodinpos(auth_1,pass,'+'),pass,ordinary(none),[pass],[identifier(rodinpos(auth_1,[],'\''),p)],[member(rodinpos(auth_1,grd1,internal1),identifier(none,p),identifier(none,'P'))],[],[assign(rodinpos(auth_1,act1,internal1),[identifier(none,sit)],[overwrite(none,identifier(none,sit),set_extension(none,[couple(none,[identifier(none,p),function(none,identifier(none,valid),[identifier(none,p)])])]))]),assign(rodinpos(auth_1,act2,'+'),[identifier(none,valid)],[overwrite(none,identifier(none,valid),set_extension(none,[couple(none,[identifier(none,p),identifier(none,nowhere)])]))])],[witness(none,identifier(none,b),equal(rodinpos(auth_1,b,'*'),identifier(none,b),function(none,identifier(none,valid),[identifier(none,p)])))]),event(rodinpos(auth_1,check,'/'),check,ordinary(none),[],[identifier(rodinpos(auth_1,[],'('),b),identifier(rodinpos(auth_1,[],'\''),p)],[member(rodinpos(auth_1,grd1,')'),identifier(none,p),identifier(none,'P')),member(rodinpos(auth_1,grd2,'*'),identifier(none,b),identifier(none,'B')),member(rodinpos(auth_1,grd3,'+'),couple(none,[identifier(none,p),identifier(none,b)]),identifier(none,aut))],[],[assign(rodinpos(auth_1,act1,','),[identifier(none,valid)],[overwrite(none,identifier(none,valid),set_extension(none,[couple(none,[identifier(none,p),identifier(none,b)])]))])],[]),event(rodinpos(auth_1,skip,'0'),skip,ordinary(none),[skip],[],[],[],[],[])])]),event_b_model(none,auth_0,[sees(none,[auth_ctx1,auth_ctx2]),variables(none,[identifier(none,sit)]),invariant(none,[subset(rodinpos(auth_0,inv1,'*'),identifier(none,sit),identifier(none,aut)),member(rodinpos(auth_0,inv2,','),identifier(none,sit),total_function(none,identifier(none,'P'),identifier(none,'B')))]),theorems(none,[]),events(none,[event(rodinpos(auth_0,'INITIALISATION','\''),'INITIALISATION',ordinary(none),[],[],[],[],[assign(rodinpos(auth_0,act1,'\''),[identifier(none,sit)],[cartesian_product(none,identifier(none,'P'),set_extension(none,[identifier(none,nowhere)]))])],[]),event(rodinpos(auth_0,pass,'+'),pass,ordinary(none),[],[identifier(rodinpos(auth_0,[],'('),b),identifier(rodinpos(auth_0,[],'\''),p)],[member(rodinpos(auth_0,grd1,')'),identifier(none,p),identifier(none,'P')),member(rodinpos(auth_0,grd2,'*'),identifier(none,b),identifier(none,'B')),member(rodinpos(auth_0,grd4,'-'),couple(none,[identifier(none,p),identifier(none,b)]),identifier(none,aut))],[],[assign(rodinpos(auth_0,act1,'+'),[identifier(none,sit)],[overwrite(none,identifier(none,sit),set_extension(none,[couple(none,[identifier(none,p),identifier(none,b)])]))])],[]),event(rodinpos(auth_0,skip,'-'),skip,anticipated(none),[],[],[],[],[],[])])])],[event_b_context(none,auth_ctx1,[extends(none,[]),constants(none,[identifier(none,aut)]),abstract_constants(none,[]),axioms(none,[member(rodinpos(auth_ctx1,axm1,'*'),identifier(none,aut),total_relation(none,identifier(none,'P'),identifier(none,'B'))),not_equal(rodinpos(auth_ctx1,axm3,','),identifier(none,aut),typeof(none,empty_set(none),pow_subset(none,cartesian_product(none,identifier(none,'P'),identifier(none,'B')))))]),theorems(none,[equal(rodinpos(auth_ctx1,axm2,'+'),domain(none,identifier(none,aut)),identifier(none,'P'))]),sets(none,[deferred_set(none,'B'),deferred_set(none,'P')])]),event_b_context(none,auth_ctx2,[extends(none,[auth_ctx1]),constants(none,[identifier(none,nowhere)]),abstract_constants(none,[]),axioms(none,[member(rodinpos(auth_ctx2,axm1,')'),identifier(none,nowhere),identifier(none,'B')),subset(rodinpos(auth_ctx2,axm2,'*'),cartesian_product(none,identifier(none,'P'),set_extension(none,[identifier(none,nowhere)])),identifier(none,aut))]),theorems(none,[]),sets(none,[])])],[exporter_version(3),po(auth_ctx1,'Theorem',[axiom(axm2)],true),po(auth_2,'Invariant establishment',[event('INITIALISATION'),event('INITIALISATION'),invariant(inv2)],true),po(auth_2,'Well-definedness of Guard',[guard(grd3),event(leave)],true),po(auth_2,'Invariant preservation',[event(pass),event(leave),invariant(inv2)],true),po(auth_2,'Action simulation',[event(pass),action(act1),event(leave)],false),po(auth_1,'Invariant establishment',[event('INITIALISATION'),event('INITIALISATION'),invariant(inv1)],true),po(auth_1,'Invariant establishment',[event('INITIALISATION'),event('INITIALISATION'),invariant(inv2)],true),po(auth_1,'Well-definedness of witness',[witness(b)],true),po(auth_1,'Invariant preservation',[event(pass),event(pass),invariant(inv1)],true),po(auth_1,'Invariant preservation',[event(pass),event(pass),invariant(inv2)],true),po(auth_1,'Guard strengthening (split)',[event(pass),guard(grd4),event(pass),event(pass)],true),po(auth_1,'Well-definedness of action',[action(act1)],true),po(auth_1,'Action simulation',[event(pass),action(act1),event(pass)],true),po(auth_1,'Invariant preservation',[event(check),invariant(inv1)],true),po(auth_1,'Invariant preservation',[event(check),invariant(inv2)],true),po(auth_0,'Invariant establishment',[event('INITIALISATION'),invariant(inv1)],true),po(auth_0,'Invariant establishment',[event('INITIALISATION'),invariant(inv2)],true),po(auth_0,'Invariant preservation',[event(pass),invariant(inv1)],true),po(auth_0,'Invariant preservation',[event(pass),invariant(inv2)],true)],_Error)).
2