| 1 | | package(load_event_b_project([event_b_model(none,'COLORING1_40',[sees(none,['COLORING0_40']),variables(none,[identifier(none,colored_nodes_m0)]),invariant(none,[member(rodinpos('COLORING1_40',inv1,'_voSs0rBvEeGAaLCkc86ytA'),identifier(none,colored_nodes_m0),partial_function(none,identifier(none,'NODES'),identifier(none,'COLORS')))]),theorems(none,[]),events(none,[event(rodinpos('COLORING1_40','INITIALISATION','\''),'INITIALISATION',ordinary(none),[],[],[],[],[assign(rodinpos('COLORING1_40',act1,'_voTT4LBvEeGAaLCkc86ytA'),[identifier(none,colored_nodes_m0)],[empty_set(none)])],[]),event(rodinpos('COLORING1_40','COLORING1','_voTT4bBvEeGAaLCkc86ytA'),'COLORING1',ordinary(none),[],[],[],[],[becomes_such(rodinpos('COLORING1_40',act1,'_voTT4rBvEeGAaLCkc86ytA'),[identifier(none,colored_nodes_m0)],conjunct(none,member(none,identifier(none,'colored_nodes_m0\''),total_function(none,identifier(none,'NODES'),identifier(none,'COLORS'))),forall(none,[identifier(none,n1)],implication(none,truth(none),forall(none,[identifier(none,n2)],implication(none,truth(none),forall(none,[identifier(none,c1)],implication(none,truth(none),forall(none,[identifier(none,c2)],implication(none,conjunct(none,not_equal(none,identifier(none,n1),identifier(none,n2)),conjunct(none,member(none,couple(none,[identifier(none,n1),identifier(none,n2)]),identifier(none,'GRAPH')),conjunct(none,member(none,couple(none,[identifier(none,n1),identifier(none,c1)]),identifier(none,'colored_nodes_m0\'')),member(none,couple(none,[identifier(none,n2),identifier(none,c2)]),identifier(none,'colored_nodes_m0\''))))),not_equal(none,identifier(none,c1),identifier(none,c2))))))))))))],[])])])],[event_b_context(none,'COLORING0_40',[extends(none,[]),constants(none,[identifier(none,'GRAPH'),identifier(none,'GRAPHD'),identifier(none,'NODES')]),axioms(none,[equal(rodinpos('COLORING0_40',axm_40_1,'_CzCf4rBvEeGAaLCkc86ytA'),identifier(none,'NODES'),interval(none,integer(none,1),integer(none,40))),equal(rodinpos('COLORING0_40',axm_40_2,'_pLx8YLBvEeGAaLCkc86ytA'),identifier(none,'GRAPHD'),set_extension(none,[couple(none,[integer(none,13),integer(none,3)]),couple(none,[integer(none,26),integer(none,14)]),couple(none,[integer(none,19),integer(none,24)]),couple(none,[integer(none,2),integer(none,13)]),couple(none,[integer(none,1),integer(none,18)]),couple(none,[integer(none,10),integer(none,20)]),couple(none,[integer(none,15),integer(none,8)]),couple(none,[integer(none,9),integer(none,8)]),couple(none,[integer(none,4),integer(none,19)]),couple(none,[integer(none,7),integer(none,3)]),couple(none,[integer(none,23),integer(none,27)]),couple(none,[integer(none,9),integer(none,7)]),couple(none,[integer(none,23),integer(none,2)]),couple(none,[integer(none,29),integer(none,17)]),couple(none,[integer(none,35),integer(none,14)]),couple(none,[integer(none,8),integer(none,1)]),couple(none,[integer(none,27),integer(none,2)]),couple(none,[integer(none,9),integer(none,36)]),couple(none,[integer(none,34),integer(none,26)]),couple(none,[integer(none,7),integer(none,26)]),couple(none,[integer(none,34),integer(none,23)]),couple(none,[integer(none,14),integer(none,20)]),couple(none,[integer(none,39),integer(none,3)]),couple(none,[integer(none,7),integer(none,31)]),couple(none,[integer(none,5),integer(none,21)]),couple(none,[integer(none,23),integer(none,11)]),couple(none,[integer(none,35),integer(none,30)]),couple(none,[integer(none,6),integer(none,11)]),couple(none,[integer(none,9),integer(none,28)]),couple(none,[integer(none,18),integer(none,30)]),couple(none,[integer(none,19),integer(none,33)]),couple(none,[integer(none,25),integer(none,28)]),couple(none,[integer(none,39),integer(none,4)]),couple(none,[integer(none,2),integer(none,19)]),couple(none,[integer(none,9),integer(none,24)]),couple(none,[integer(none,8),integer(none,26)]),couple(none,[integer(none,10),integer(none,6)]),couple(none,[integer(none,22),integer(none,25)]),couple(none,[integer(none,32),integer(none,25)]),couple(none,[integer(none,23),integer(none,40)]),couple(none,[integer(none,30),integer(none,17)]),couple(none,[integer(none,2),integer(none,4)]),couple(none,[integer(none,5),integer(none,24)]),couple(none,[integer(none,27),integer(none,36)]),couple(none,[integer(none,20),integer(none,38)]),couple(none,[integer(none,31),integer(none,38)]),couple(none,[integer(none,35),integer(none,9)]),couple(none,[integer(none,19),integer(none,5)]),couple(none,[integer(none,8),integer(none,16)]),couple(none,[integer(none,18),integer(none,15)]),couple(none,[integer(none,35),integer(none,4)]),couple(none,[integer(none,19),integer(none,21)]),couple(none,[integer(none,15),integer(none,37)]),couple(none,[integer(none,34),integer(none,24)]),couple(none,[integer(none,6),integer(none,8)]),couple(none,[integer(none,8),integer(none,36)]),couple(none,[integer(none,2),integer(none,1)]),couple(none,[integer(none,23),integer(none,13)]),couple(none,[integer(none,13),integer(none,35)]),couple(none,[integer(none,36),integer(none,25)]),couple(none,[integer(none,26),integer(none,20)]),couple(none,[integer(none,32),integer(none,36)]),couple(none,[integer(none,24),integer(none,2)]),couple(none,[integer(none,9),integer(none,17)]),couple(none,[integer(none,38),integer(none,27)]),couple(none,[integer(none,18),integer(none,38)]),couple(none,[integer(none,36),integer(none,20)]),couple(none,[integer(none,34),integer(none,32)]),couple(none,[integer(none,8),integer(none,5)]),couple(none,[integer(none,5),integer(none,1)]),couple(none,[integer(none,28),integer(none,7)]),couple(none,[integer(none,33),integer(none,8)]),couple(none,[integer(none,5),integer(none,22)]),couple(none,[integer(none,31),integer(none,9)]),couple(none,[integer(none,30),integer(none,40)]),couple(none,[integer(none,26),integer(none,33)]),couple(none,[integer(none,32),integer(none,1)]),couple(none,[integer(none,6),integer(none,19)]),couple(none,[integer(none,14),integer(none,5)]),couple(none,[integer(none,8),integer(none,18)]),couple(none,[integer(none,40),integer(none,22)]),couple(none,[integer(none,4),integer(none,5)]),couple(none,[integer(none,5),integer(none,13)]),couple(none,[integer(none,34),integer(none,40)]),couple(none,[integer(none,12),integer(none,15)]),couple(none,[integer(none,25),integer(none,14)]),couple(none,[integer(none,3),integer(none,35)]),couple(none,[integer(none,10),integer(none,23)]),couple(none,[integer(none,18),integer(none,26)]),couple(none,[integer(none,31),integer(none,15)]),couple(none,[integer(none,13),integer(none,38)]),couple(none,[integer(none,13),integer(none,18)]),couple(none,[integer(none,20),integer(none,22)]),couple(none,[integer(none,18),integer(none,9)]),couple(none,[integer(none,11),integer(none,13)]),couple(none,[integer(none,40),integer(none,25)]),couple(none,[integer(none,40),integer(none,5)]),couple(none,[integer(none,28),integer(none,20)]),couple(none,[integer(none,37),integer(none,28)]),couple(none,[integer(none,3),integer(none,26)]),couple(none,[integer(none,38),integer(none,4)]),couple(none,[integer(none,3),integer(none,12)]),couple(none,[integer(none,5),integer(none,6)]),couple(none,[integer(none,30),integer(none,26)]),couple(none,[integer(none,32),integer(none,26)]),couple(none,[integer(none,7),integer(none,17)]),couple(none,[integer(none,31),integer(none,32)]),couple(none,[integer(none,22),integer(none,37)]),couple(none,[integer(none,38),integer(none,26)]),couple(none,[integer(none,3),integer(none,23)]),couple(none,[integer(none,34),integer(none,3)]),couple(none,[integer(none,6),integer(none,35)]),couple(none,[integer(none,34),integer(none,30)]),couple(none,[integer(none,23),integer(none,4)]),couple(none,[integer(none,23),integer(none,15)]),couple(none,[integer(none,10),integer(none,17)]),couple(none,[integer(none,12),integer(none,37)]),couple(none,[integer(none,40),integer(none,37)]),couple(none,[integer(none,28),integer(none,34)]),couple(none,[integer(none,38),integer(none,5)]),couple(none,[integer(none,16),integer(none,29)]),couple(none,[integer(none,5),integer(none,25)]),couple(none,[integer(none,21),integer(none,30)]),couple(none,[integer(none,37),integer(none,39)]),couple(none,[integer(none,32),integer(none,7)]),couple(none,[integer(none,7),integer(none,13)]),couple(none,[integer(none,15),integer(none,20)]),couple(none,[integer(none,39),integer(none,13)]),couple(none,[integer(none,26),integer(none,36)]),couple(none,[integer(none,18),integer(none,12)]),couple(none,[integer(none,4),integer(none,6)]),couple(none,[integer(none,21),integer(none,39)]),couple(none,[integer(none,21),integer(none,7)]),couple(none,[integer(none,29),integer(none,36)]),couple(none,[integer(none,11),integer(none,21)]),couple(none,[integer(none,20),integer(none,11)]),couple(none,[integer(none,22),integer(none,36)]),couple(none,[integer(none,24),integer(none,23)]),couple(none,[integer(none,38),integer(none,24)]),couple(none,[integer(none,4),integer(none,10)]),couple(none,[integer(none,20),integer(none,23)]),couple(none,[integer(none,38),integer(none,36)]),couple(none,[integer(none,16),integer(none,23)]),couple(none,[integer(none,12),integer(none,30)]),couple(none,[integer(none,17),integer(none,6)]),couple(none,[integer(none,29),integer(none,10)]),couple(none,[integer(none,10),integer(none,31)]),couple(none,[integer(none,7),integer(none,37)]),couple(none,[integer(none,40),integer(none,19)]),couple(none,[integer(none,27),integer(none,18)]),couple(none,[integer(none,12),integer(none,16)]),couple(none,[integer(none,6),integer(none,7)]),couple(none,[integer(none,8),integer(none,30)]),couple(none,[integer(none,25),integer(none,27)]),couple(none,[integer(none,38),integer(none,21)]),couple(none,[integer(none,27),integer(none,31)]),couple(none,[integer(none,4),integer(none,31)]),couple(none,[integer(none,5),integer(none,9)]),couple(none,[integer(none,23),integer(none,29)]),couple(none,[integer(none,35),integer(none,8)]),couple(none,[integer(none,11),integer(none,27)]),couple(none,[integer(none,17),integer(none,21)]),couple(none,[integer(none,26),integer(none,37)]),couple(none,[integer(none,3),integer(none,6)]),couple(none,[integer(none,5),integer(none,27)]),couple(none,[integer(none,9),integer(none,6)]),couple(none,[integer(none,26),integer(none,27)]),couple(none,[integer(none,5),integer(none,12)]),couple(none,[integer(none,14),integer(none,30)]),couple(none,[integer(none,35),integer(none,29)]),couple(none,[integer(none,10),integer(none,11)]),couple(none,[integer(none,38),integer(none,8)]),couple(none,[integer(none,36),integer(none,28)]),couple(none,[integer(none,1),integer(none,14)]),couple(none,[integer(none,31),integer(none,37)]),couple(none,[integer(none,13),integer(none,34)]),couple(none,[integer(none,26),integer(none,2)]),couple(none,[integer(none,12),integer(none,7)]),couple(none,[integer(none,34),integer(none,5)]),couple(none,[integer(none,3),integer(none,19)]),couple(none,[integer(none,15),integer(none,16)]),couple(none,[integer(none,20),integer(none,39)]),couple(none,[integer(none,19),integer(none,10)]),couple(none,[integer(none,12),integer(none,23)]),couple(none,[integer(none,6),integer(none,30)]),couple(none,[integer(none,11),integer(none,2)]),couple(none,[integer(none,25),integer(none,34)]),couple(none,[integer(none,24),integer(none,10)]),couple(none,[integer(none,40),integer(none,38)]),couple(none,[integer(none,24),integer(none,13)]),couple(none,[integer(none,35),integer(none,37)]),couple(none,[integer(none,37),integer(none,2)]),couple(none,[integer(none,33),integer(none,2)]),couple(none,[integer(none,31),integer(none,22)]),couple(none,[integer(none,15),integer(none,11)]),couple(none,[integer(none,22),integer(none,29)]),couple(none,[integer(none,9),integer(none,34)]),couple(none,[integer(none,34),integer(none,8)]),couple(none,[integer(none,17),integer(none,12)]),couple(none,[integer(none,1),integer(none,29)])])),equal(rodinpos('COLORING0_40',axm40_3,'_ABfv4LBwEeGAaLCkc86ytA'),identifier(none,'GRAPH'),union(none,identifier(none,'GRAPHD'),reverse(none,identifier(none,'GRAPHD')))),not_equal(rodinpos('COLORING0_40',axm1,'_CzDG8LBvEeGAaLCkc86ytA'),identifier(none,'NODES'),empty_set(none)),member(rodinpos('COLORING0_40',axm2,'_CzDG8bBvEeGAaLCkc86ytA'),identifier(none,'GRAPH'),relations(none,identifier(none,'NODES'),identifier(none,'NODES'))),not_equal(rodinpos('COLORING0_40',axm3,'_CzDG8rBvEeGAaLCkc86ytA'),identifier(none,'GRAPH'),empty_set(none)),finite(rodinpos('COLORING0_40',axm0,'_CzDG87BvEeGAaLCkc86ytA'),identifier(none,'COLORS')),not_equal(rodinpos('COLORING0_40',axm4,'_CzDG9LBvEeGAaLCkc86ytA'),identifier(none,'COLORS'),empty_set(none)),forall(rodinpos('COLORING0_40',axm5,'_CzDuALBvEeGAaLCkc86ytA'),[identifier(none,n)],implication(none,member(none,identifier(none,n),identifier(none,'NODES')),member(none,identifier(none,n),domain(none,identifier(none,'GRAPH'))))),equal(rodinpos('COLORING0_40',axm6,'_CzDuAbBvEeGAaLCkc86ytA'),intersection(none,domain_restriction(none,identifier(none,'NODES'),event_b_identity(none)),identifier(none,'GRAPH')),empty_set(none)),equal(rodinpos('COLORING0_40',axm7,'_CzDuArBvEeGAaLCkc86ytA'),identifier(none,'GRAPH'),reverse(none,identifier(none,'GRAPH'))) |