1		package(load_event_b_project([event_b_model(none,'MultiplePrinters',[sees(none,['C1']),variables(none,[identifier(none,job),identifier(none,position),identifier(none,queue)]),invariant(none,[subset(rodinpos('MultiplePrinters',inv1,'_dYP0oXqpEeKnYblMwWSB1g'),identifier(none,job),identifier(none,'JOB')),member(rodinpos('MultiplePrinters',inv3,'_dYP0o3qpEeKnYblMwWSB1g'),identifier(none,position),total_function(none,identifier(none,queue),relations(none,identifier(none,'JOB'),identifier(none,'POSITION')))),forall(rodinpos('MultiplePrinters',inv4,'_Alvq4HqvEeKnYblMwWSB1g'),[identifier(none,q)],implication(none,member(none,identifier(none,q),identifier(none,queue)),member(none,function(none,identifier(none,position),[identifier(none,q)]),partial_injection(none,identifier(none,job),identifier(none,'POSITION')))))]),theorems(none,[subset(rodinpos('MultiplePrinters',inv2,'_dYP0onqpEeKnYblMwWSB1g'),identifier(none,queue),identifier(none,'QUEUE'))]),events(none,[event(rodinpos('MultiplePrinters','INITIALISATION','_dYQbsXqpEeKnYblMwWSB1g'),'INITIALISATION',ordinary(none),[],[],[],[],[assign(rodinpos('MultiplePrinters',act1,'_dYQbsnqpEeKnYblMwWSB1g'),[identifier(none,job)],[empty_set(none)]),assign(rodinpos('MultiplePrinters',act2,'_dYQbs3qpEeKnYblMwWSB1g'),[identifier(none,position)],[empty_set(none)]),assign(rodinpos('MultiplePrinters',act4,'_NLOW8HqqEeKnYblMwWSB1g'),[identifier(none,queue)],[empty_set(none)])],[])])])],[event_b_context(none,'C1',[extends(none,[]),constants(none,[identifier(none,'POSITION')]),abstract_constants(none,[]),axioms(none,[equal(rodinpos('C1',axm1,'_Bs8vEHqlEeKnYblMwWSB1g'),identifier(none,'POSITION'),natural_set(none))]),theorems(none,[]),sets(none,[deferred_set(none,'DOCUMENT'),deferred_set(none,'JOB'),deferred_set(none,'PRINTER'),deferred_set(none,'QUEUE'),deferred_set(none,'USER')])])],[exporter_version(3),po('MultiplePrinters','Well-definedness of Invariant',[invariant(inv4)],true),po('MultiplePrinters','Invariant establishment',[event('INITIALISATION'),invariant(inv3)],true),po('MultiplePrinters','Invariant establishment',[event('INITIALISATION'),invariant(inv4)],true)],_Error)).
2