1		package(load_event_b_project([event_b_model(none,'M0_v4',[sees(none,[c,'Coloration','Coloration_finite']),variables(none,[identifier(none,node_color),identifier(none,t)]),invariant(none,[member(rodinpos('M0_v4',inv1,'_Wx9GhOPeEeaU86Rx_hNGRg'),identifier(none,node_color),relations(none,cartesian_product(none,identifier(none,'V'),interval(none,integer(none,0),identifier(none,t))),identifier(none,colors_list)))]),theorems(none,[]),events(none,[event(rodinpos('M0_v4','INITIALISATION','\''),'INITIALISATION',ordinary(none),[],[],[],[],[becomes_such(rodinpos('M0_v4',act1,'_Wx9GgePeEeaU86Rx_hNGRg'),[identifier(none,t),identifier(none,node_color)],conjunct(none,equal(none,identifier(none,'t\''),integer(none,0)),equal(none,identifier(none,'node_color\''),cartesian_product(none,cartesian_product(none,identifier(none,'V'),set_extension(none,[integer(none,0)])),identifier(none,colors_list)))))],[]),event(rodinpos('M0_v4',reset,'_Wx9GhePeEeaU86Rx_hNGRg'),reset,ordinary(none),[],[],[],[],[becomes_such(rodinpos('M0_v4',act1,'_Wx9GhuPeEeaU86Rx_hNGRg'),[identifier(none,t),identifier(none,node_color)],conjunct(none,equal(none,identifier(none,'t\''),integer(none,0)),equal(none,identifier(none,'node_color\''),cartesian_product(none,cartesian_product(none,identifier(none,'V'),set_extension(none,[integer(none,0)])),identifier(none,colors_list)))))],[])])])],[event_b_context(none,c,[extends(none,[]),constants(none,[identifier(none,tmax)]),abstract_constants(none,[]),axioms(none,[member(rodinpos(c,axm1,'_P2288BS1EeSqG9PpDkqwdw'),identifier(none,tmax),set_subtraction(none,natural_set(none),set_extension(none,[integer(none,0)]))),finite(rodinpos(c,axm2,'_P2288BS1EeSqG9PpDkqwdx'),identifier(none,'V'))]),theorems(none,[]),sets(none,[deferred_set(none,'V')])]),event_b_context(none,'Coloration',[extends(none,[c]),constants(none,[identifier(none,color)]),abstract_constants(none,[]),axioms(none,[finite(rodinpos('Coloration',axm3,'0'),identifier(none,colors_list)),less_equal(rodinpos('Coloration',axm1,'*'),card(none,identifier(none,colors_list)),card(none,identifier(none,'V'))),member(rodinpos('Coloration',axm2,'-'),identifier(none,color),total_bijection(none,interval(none,integer(none,1),card(none,identifier(none,'V'))),identifier(none,colors_list))),not_equal(rodinpos('Coloration',axm4,'/'),identifier(none,colors_list),typeof(none,empty_set(none),pow_subset(none,identifier(none,colors_list))))]),theorems(none,[]),sets(none,[deferred_set(none,colors_list)])]),event_b_context(none,'Coloration_finite',[extends(none,['Coloration']),constants(none,[]),abstract_constants(none,[]),axioms(none,[conjunct(rodinpos('Coloration_finite',prob,'_ssWhQOPeEeaU86Rx_hNGRg'),equal(none,card(none,identifier(none,'V')),integer(none,3)),equal(none,identifier(none,tmax),integer(none,3)))]),theorems(none,[]),sets(none,[])])],[exporter_version(3),po('Coloration','Well-definedness of Axiom',[axiom(axm1)],true),po('Coloration','Well-definedness of Axiom',[axiom(axm2)],true),po('Coloration_finite','Well-definedness of Axiom',[axiom(prob)],false),po('M0_v4','Invariant establishment',[event('INITIALISATION'),invariant(inv1)],false),po('M0_v4','Feasibility of action',[action(act1)],false),po('M0_v4','Invariant preservation',[event(reset),invariant(inv1)],false),po('M0_v4','Feasibility of action',[action(act1)],false)],_Error)).
2