1		package(load_event_b_project([event_b_model(none,sort_m2_data400,[sees(none,[sort_c0,sort_c0_data400]),refines(none,sort_m2),variables(none,[identifier(none,g),identifier(none,j),identifier(none,k),identifier(none,l)]),invariant(none,[]),theorems(none,[]),events(none,[event(rodinpos(sort_m2_data400,'INITIALISATION','_KMt90YmlEeKZae4Iol7iJB'),'INITIALISATION',ordinary(none),['INITIALISATION'],[],[],[],[assign(rodinpos(sort_m2_data400,act1,internal_element1),[identifier(none,g)],[identifier(none,f)]),assign(rodinpos(sort_m2_data400,act2,internal_element2),[identifier(none,k)],[integer(none,1)]),assign(rodinpos(sort_m2_data400,act3,internal_element3),[identifier(none,l)],[integer(none,1)]),assign(rodinpos(sort_m2_data400,act4,internal_element4),[identifier(none,j)],[integer(none,1)])],[]),event(rodinpos(sort_m2_data400,progress,'_KMt90YmlEeKZae4Iol7iJC'),progress,ordinary(none),[progress],[],[not_equal(rodinpos(sort_m2_data400,grd1,internal_element1),identifier(none,k),identifier(none,n)),equal(rodinpos(sort_m2_data400,grd2,internal_element3),identifier(none,j),identifier(none,n))],[],[assign(rodinpos(sort_m2_data400,act1,internal_element1),[identifier(none,g)],[overwrite(none,identifier(none,g),overwrite(none,set_extension(none,[couple(none,[identifier(none,k),function(none,identifier(none,g),[identifier(none,l)])])]),set_extension(none,[couple(none,[identifier(none,l),function(none,identifier(none,g),[identifier(none,k)])])])))]),assign(rodinpos(sort_m2_data400,act2,internal_element2),[identifier(none,k)],[add(none,identifier(none,k),integer(none,1))]),assign(rodinpos(sort_m2_data400,act3,internal_element3),[identifier(none,j)],[add(none,identifier(none,k),integer(none,1))]),assign(rodinpos(sort_m2_data400,act4,internal_element4),[identifier(none,l)],[add(none,identifier(none,k),integer(none,1))])],[]),event(rodinpos(sort_m2_data400,prog1,'_KMt90YmlEeKZae4Iol7iJD'),prog1,ordinary(none),[prog1],[],[not_equal(rodinpos(sort_m2_data400,grd1,internal_element1),identifier(none,k),identifier(none,n)),not_equal(rodinpos(sort_m2_data400,grd2,internal_element2),identifier(none,j),identifier(none,n)),less_equal(rodinpos(sort_m2_data400,grd3,internal_element3),function(none,identifier(none,g),[identifier(none,l)]),function(none,identifier(none,g),[add(none,identifier(none,j),integer(none,1))]))],[],[assign(rodinpos(sort_m2_data400,act1,internal_element1),[identifier(none,j)],[add(none,identifier(none,j),integer(none,1))])],[]),event(rodinpos(sort_m2_data400,prog2,'_KMt90YmlEeKZae4Iol7iJE'),prog2,ordinary(none),[prog2],[],[not_equal(rodinpos(sort_m2_data400,grd1,internal_element1),identifier(none,k),identifier(none,n)),not_equal(rodinpos(sort_m2_data400,grd2,internal_element2),identifier(none,j),identifier(none,n)),greater(rodinpos(sort_m2_data400,grd3,internal_element3),function(none,identifier(none,g),[identifier(none,l)]),function(none,identifier(none,g),[add(none,identifier(none,j),integer(none,1))]))],[],[assign(rodinpos(sort_m2_data400,act1,internal_element1),[identifier(none,j)],[add(none,identifier(none,j),integer(none,1))]),assign(rodinpos(sort_m2_data400,act2,internal_element2),[identifier(none,l)],[add(none,identifier(none,j),integer(none,1))])],[]),event(rodinpos(sort_m2_data400,final_evt,'_KMt90YmlEeKZae4Iol7iJF'),final_evt,ordinary(none),[final_evt],[],[equal(rodinpos(sort_m2_data400,grd1,'_KMxBIYmlEeKZae4Iol7iJA'),identifier(none,k),identifier(none,n))],[],[],[])])]),event_b_model(none,sort_m2,[sees(none,[sort_c0]),refines(none,sort_m1),variables(none,[identifier(none,g),identifier(none,j),identifier(none,k),identifier(none,l)]),invariant(none,[member(rodinpos(sort_m2,inv1_m2,internal_element1I),identifier(none,j),interval(none,identifier(none,k),identifier(none,n))),member(rodinpos(sort_m2,inv2_m2,internal_element3I),identifier(none,l),interval(none,identifier(none,k),identifier(none,j))),equal(rodinpos(sort_m2,inv3_m2,internal_element2I),function(none,identifier(none,g),[identifier(none,l)]),min(none,image(none,identifier(none,g),interval(none,identifier(none,k),identifier(none,j)))))]),theorems(none,[]),variant(none,minus(none,identifier(none,n),identifier(none,j))),events(none,[event(rodinpos(sort_m2,'INITIALISATION',internal_evt1),'INITIALISATION',ordinary(none),['INITIALISATION'],[],[],[],[assign(rodinpos(sort_m2,act1,internal_element1),[identifier(none,g)],[identifier(none,f)]),assign(rodinpos(sort_m2,act2,internal_element2),[identifier(none,k)],[integer(none,1)]),assign(rodinpos(sort_m2,act3,internal_element3),[identifier(none,l)],[integer(none,1)]),assign(rodinpos(sort_m2,act4,internal_element4),[identifier(none,j)],[integer(none,1)])],[]),event(rodinpos(sort_m2,progress,internal_element2),progress,ordinary(none),[progress],[],[not_equal(rodinpos(sort_m2,grd1,internal_element1),identifier(none,k),identifier(none,n)),equal(rodinpos(sort_m2,grd2,internal_element3),identifier(none,j),identifier(none,n))],[],[assign(rodinpos(sort_m2,act1,internal_element1),[identifier(none,g)],[overwrite(none,identifier(none,g),overwrite(none,set_extension(none,[couple(none,[identifier(none,k),function(none,identifier(none,g),[identifier(none,l)])])]),set_extension(none,[couple(none,[identifier(none,l),function(none,identifier(none,g),[identifier(none,k)])])])))]),assign(rodinpos(sort_m2,act2,internal_element2),[identifier(none,k)],[add(none,identifier(none,k),integer(none,1))]),assign(rodinpos(sort_m2,act3,internal_element3),[identifier(none,j)],[add(none,identifier(none,k),integer(none,1))]),assign(rodinpos(sort_m2,act4,internal_element4),[identifier(none,l)],[add(none,identifier(none,k),integer(none,1))])],[]),event(rodinpos(sort_m2,prog1,internal_element3),prog1,convergent(none),[prog],[],[not_equal(rodinpos(sort_m2,grd1,internal_element1),identifier(none,k),identifier(none,n)),not_equal(rodinpos(sort_m2,grd2,internal_element2),identifier(none,j),identifier(none,n)),less_equal(rodinpos(sort_m2,grd3,internal_element3),function(none,identifier(none,g),[identifier(none,l)]),function(none,identifier(none,g),[add(none,identifier(none,j),integer(none,1))]))],[],[assign(rodinpos(sort_m2,act1,internal_element1),[identifier(none,j)],[add(none,identifier(none,j),integer(none,1))])],[]),event(rodinpos(sort_m2,prog2,internal_element4),prog2,convergent(none),[prog],[],[not_equal(rodinpos(sort_m2,grd1,internal_element1),identifier(none,k),identifier(none,n)),not_equal(rodinpos(sort_m2,grd2,internal_element2),identifier(none,j),identifier(none,n)),greater(rodinpos(sort_m2,grd3,internal_element3),function(none,identifier(none,g),[identifier(none,l)]),function(none,identifier(none,g),[add(none,identifier(none,j),integer(none,1))]))],[],[assign(rodinpos(sort_m2,act1,internal_element1),[identifier(none,j)],[add(none,identifier(none,j),integer(none,1))]),assign(rodinpos(sort_m2,act2,internal_element2),[identifier(none,l)],[add(none,identifier(none,j),integer(none,1))])],[]),event(rodinpos(sort_m2,final_evt,'_KMwaEYmlEeKZae4Iol7iJA'),final_evt,ordinary(none),[final_evt],[],[equal(rodinpos(sort_m2,grd1,'_KMxBIYmlEeKZae4Iol7iJA'),identifier(none,k),identifier(none,n))],[],[],[])])]),event_b_model(none,sort_m1,[sees(none,[sort_c0]),refines(none,sort_m0),variables(none,[identifier(none,g),identifier(none,k),identifier(none,l)]),invariant(none,[member(rodinpos(sort_m1,inv1_m1,internal_element1I),identifier(none,g),total_injection(none,interval(none,integer(none,1),identifier(none,n)),natural_set(none))),equal(rodinpos(sort_m1,inv2_m1,internal_element2I),range(none,identifier(none,g)),range(none,identifier(none,f))),member(rodinpos(sort_m1,inv3_m1,internal_element3I),identifier(none,k),interval(none,integer(none,1),identifier(none,n))),forall(rodinpos(sort_m1,inv4_m1,internal_element4I),[identifier(none,i_f),identifier(none,j_f)],implication(none,conjunct(none,member(none,identifier(none,i_f),integer_set(none)),conjunct(none,member(none,identifier(none,j_f),integer_set(none)),conjunct(none,member(none,identifier(none,i_f),interval(none,integer(none,1),minus(none,identifier(none,k),integer(none,1)))),member(none,identifier(none,j_f),interval(none,add(none,identifier(none,i_f),integer(none,1)),identifier(none,n)))))),less(none,function(none,identifier(none,g),[identifier(none,i_f)]),function(none,identifier(none,g),[identifier(none,j_f)])))),member(rodinpos(sort_m1,inv5_m1,internal_element5I),identifier(none,l),natural_set(none))]),theorems(none,[forall(rodinpos(sort_m1,thm1_m1,internal_element1T),[identifier(none,a_f),identifier(none,b_f)],implication(none,conjunct(none,member(none,identifier(none,a_f),integer_set(none)),conjunct(none,member(none,identifier(none,b_f),integer_set(none)),conjunct(none,member(none,identifier(none,a_f),interval(none,integer(none,1),identifier(none,n))),conjunct(none,member(none,identifier(none,b_f),interval(none,integer(none,1),identifier(none,n))),not_equal(none,identifier(none,a_f),identifier(none,b_f)))))),equal(none,overwrite(none,identifier(none,g),overwrite(none,set_extension(none,[couple(none,[identifier(none,a_f),function(none,identifier(none,g),[identifier(none,b_f)])])]),set_extension(none,[couple(none,[identifier(none,b_f),function(none,identifier(none,g),[identifier(none,a_f)])])]))),union(none,domain_subtraction(none,set_extension(none,[identifier(none,a_f),identifier(none,b_f)]),identifier(none,g)),set_extension(none,[couple(none,[identifier(none,a_f),function(none,identifier(none,g),[identifier(none,b_f)])]),couple(none,[identifier(none,b_f),function(none,identifier(none,g),[identifier(none,a_f)])])]))))),forall(rodinpos(sort_m1,thm2_m1,internal_element2T),[identifier(none,a_f),identifier(none,b_f)],implication(none,conjunct(none,member(none,identifier(none,a_f),integer_set(none)),conjunct(none,member(none,identifier(none,b_f),integer_set(none)),conjunct(none,member(none,identifier(none,a_f),interval(none,integer(none,1),identifier(none,n))),conjunct(none,member(none,identifier(none,b_f),interval(none,integer(none,1),identifier(none,n))),not_equal(none,identifier(none,a_f),identifier(none,b_f)))))),member(none,set_extension(none,[couple(none,[identifier(none,a_f),function(none,identifier(none,g),[identifier(none,b_f)])]),couple(none,[identifier(none,b_f),function(none,identifier(none,g),[identifier(none,a_f)])])]),partial_injection(none,interval(none,integer(none,1),identifier(none,n)),natural_set(none))))),forall(rodinpos(sort_m1,thm3_m1,internal_element3T),[identifier(none,a_f),identifier(none,b_f)],implication(none,conjunct(none,member(none,identifier(none,a_f),integer_set(none)),conjunct(none,member(none,identifier(none,b_f),integer_set(none)),conjunct(none,member(none,identifier(none,a_f),interval(none,integer(none,1),identifier(none,n))),conjunct(none,member(none,identifier(none,b_f),interval(none,integer(none,1),identifier(none,n))),not_equal(none,identifier(none,a_f),identifier(none,b_f)))))),member(none,domain_subtraction(none,set_extension(none,[identifier(none,a_f),identifier(none,b_f)]),identifier(none,g)),partial_injection(none,interval(none,integer(none,1),identifier(none,n)),natural_set(none))))),forall(rodinpos(sort_m1,thm4_m1,internal_element4T),[identifier(none,a_f),identifier(none,b_f)],implication(none,conjunct(none,member(none,identifier(none,a_f),integer_set(none)),conjunct(none,member(none,identifier(none,b_f),integer_set(none)),conjunct(none,member(none,identifier(none,a_f),interval(none,integer(none,1),identifier(none,n))),conjunct(none,member(none,identifier(none,b_f),interval(none,integer(none,1),identifier(none,n))),not_equal(none,identifier(none,a_f),identifier(none,b_f)))))),equal(none,domain(none,union(none,domain_subtraction(none,set_extension(none,[identifier(none,a_f),identifier(none,b_f)]),identifier(none,g)),set_extension(none,[couple(none,[identifier(none,a_f),function(none,identifier(none,g),[identifier(none,b_f)])]),couple(none,[identifier(none,b_f),function(none,identifier(none,g),[identifier(none,a_f)])])]))),interval(none,integer(none,1),identifier(none,n))))),forall(rodinpos(sort_m1,thm5_m1,internal_element5T),[identifier(none,a_f),identifier(none,b_f)],implication(none,conjunct(none,member(none,identifier(none,a_f),integer_set(none)),conjunct(none,member(none,identifier(none,b_f),integer_set(none)),conjunct(none,member(none,identifier(none,a_f),interval(none,integer(none,1),identifier(none,n))),conjunct(none,member(none,identifier(none,b_f),interval(none,integer(none,1),identifier(none,n))),not_equal(none,identifier(none,a_f),identifier(none,b_f)))))),equal(none,intersection(none,domain(none,domain_subtraction(none,set_extension(none,[identifier(none,a_f),identifier(none,b_f)]),identifier(none,g))),domain(none,set_extension(none,[couple(none,[identifier(none,a_f),function(none,identifier(none,g),[identifier(none,b_f)])]),couple(none,[identifier(none,b_f),function(none,identifier(none,g),[identifier(none,a_f)])])]))),typeof(none,empty_set(none),pow_subset(none,integer_set(none)))))),forall(rodinpos(sort_m1,thm6_m1,internal_element6T),[identifier(none,a_f),identifier(none,b_f)],implication(none,conjunct(none,member(none,identifier(none,a_f),integer_set(none)),conjunct(none,member(none,identifier(none,b_f),integer_set(none)),conjunct(none,member(none,identifier(none,a_f),interval(none,integer(none,1),identifier(none,n))),conjunct(none,member(none,identifier(none,b_f),interval(none,integer(none,1),identifier(none,n))),not_equal(none,identifier(none,a_f),identifier(none,b_f)))))),equal(none,intersection(none,range(none,domain_subtraction(none,set_extension(none,[identifier(none,a_f),identifier(none,b_f)]),identifier(none,g))),range(none,set_extension(none,[couple(none,[identifier(none,a_f),function(none,identifier(none,g),[identifier(none,b_f)])]),couple(none,[identifier(none,b_f),function(none,identifier(none,g),[identifier(none,a_f)])])]))),typeof(none,empty_set(none),pow_subset(none,integer_set(none))))))]),variant(none,minus(none,identifier(none,n),identifier(none,k))),events(none,[event(rodinpos(sort_m1,'INITIALISATION',internal_evt1),'INITIALISATION',ordinary(none),['INITIALISATION'],[],[],[],[assign(rodinpos(sort_m1,act1,internal_element1),[identifier(none,g)],[identifier(none,f)]),assign(rodinpos(sort_m1,act2,internal_element2),[identifier(none,k)],[integer(none,1)]),becomes_element_of(rodinpos(sort_m1,act3,internal_element3),[identifier(none,l)],natural_set(none))],[]),event(rodinpos(sort_m1,progress,internal_element2),progress,convergent(none),[progress],[],[not_equal(rodinpos(sort_m1,grd1,internal_element1),identifier(none,k),identifier(none,n)),member(rodinpos(sort_m1,grd2,internal_element3),identifier(none,l),interval(none,identifier(none,k),identifier(none,n))),equal(rodinpos(sort_m1,grd3,internal_element2),function(none,identifier(none,g),[identifier(none,l)]),min(none,image(none,identifier(none,g),interval(none,identifier(none,k),identifier(none,n)))))],[],[assign(rodinpos(sort_m1,act1,internal_element1),[identifier(none,g)],[overwrite(none,identifier(none,g),overwrite(none,set_extension(none,[couple(none,[identifier(none,k),function(none,identifier(none,g),[identifier(none,l)])])]),set_extension(none,[couple(none,[identifier(none,l),function(none,identifier(none,g),[identifier(none,k)])])])))]),assign(rodinpos(sort_m1,act2,internal_element2),[identifier(none,k)],[add(none,identifier(none,k),integer(none,1))]),becomes_element_of(rodinpos(sort_m1,act3,internal_element3),[identifier(none,l)],natural_set(none))],[]),event(rodinpos(sort_m1,prog,internal_element3),prog,anticipated(none),[],[],[],[],[becomes_element_of(rodinpos(sort_m1,act1,internal_element1),[identifier(none,l)],natural_set(none))],[]),event(rodinpos(sort_m1,final_evt,'_I_PeEImlEeKZae4Iol7iJA'),final_evt,ordinary(none),[final_evt],[],[equal(rodinpos(sort_m1,grd1,'_I_QFIYmlEeKZae4Iol7iJA'),identifier(none,k),identifier(none,n))],[],[],[])])]),event_b_model(none,sort_m0,[sees(none,[sort_c0]),variables(none,[identifier(none,g)]),invariant(none,[member(rodinpos(sort_m0,inv1,internal_element1I),identifier(none,g),relations(none,natural_set(none),natural_set(none)))]),theorems(none,[]),events(none,[event(rodinpos(sort_m0,'INITIALISATION',internal_evt1),'INITIALISATION',ordinary(none),[],[],[],[],[becomes_element_of(rodinpos(sort_m0,act1,internal_element1),[identifier(none,g)],relations(none,natural_set(none),natural_set(none)))],[]),event(rodinpos(sort_m0,progress,internal_element2),progress,anticipated(none),[],[],[],[],[becomes_element_of(rodinpos(sort_m0,act1,internal_element1),[identifier(none,g)],relations(none,natural_set(none),natural_set(none)))],[]),event(rodinpos(sort_m0,final_evt,'_IFOs4ImlEeKZae4Iol7iJA'),final_evt,ordinary(none),[],[],[member(rodinpos(sort_m0,grd1,'_IFPT8ImlEeKZae4Iol7iJA'),identifier(none,g),total_injection(none,interval(none,integer(none,1),identifier(none,n)),natural_set(none))),equal(rodinpos(sort_m0,grd2,'_IFPT8YmlEeKZae4Iol7iJA'),range(none,identifier(none,g)),range(none,identifier(none,f))),forall(rodinpos(sort_m0,grd3,'_IFPT8omlEeKZae4Iol7iJA'),[identifier(none,i_f),identifier(none,j_f)],implication(none,conjunct(none,member(none,identifier(none,i_f),integer_set(none)),conjunct(none,member(none,identifier(none,j_f),integer_set(none)),conjunct(none,member(none,identifier(none,i_f),interval(none,integer(none,1),minus(none,identifier(none,n),integer(none,1)))),member(none,identifier(none,j_f),interval(none,add(none,identifier(none,i_f),integer(none,1)),identifier(none,n)))))),less(none,function(none,identifier(none,g),[identifier(none,i_f)]),function(none,identifier(none,g),[identifier(none,j_f)]))))],[],[],[])])])],[event_b_context(none,sort_c0,[extends(none,[]),constants(none,[identifier(none,f),identifier(none,n)]),abstract_constants(none,[]),axioms(none,[greater(rodinpos(sort_c0,axm1,internal_element1A),identifier(none,n),integer(none,0)),member(rodinpos(sort_c0,axm2,internal_element2A),identifier(none,f),total_injection(none,interval(none,integer(none,1),identifier(none,n)),natural_set(none)))]),theorems(none,[]),sets(none,[])]),event_b_context(none,sort_c0_data400,[extends(none,[sort_c0]),constants(none,[]),abstract_constants(none,[]),axioms(none,[equal(rodinpos(sort_c0_data400,prob_f,'_ikkRUBT7EeaWueYwVXo3Zg'),identifier(none,f),event_b_comprehension_set(none,[identifier(none,i)],couple(none,[identifier(none,i),minus(none,integer(none,500),identifier(none,i))]),conjunct(none,member(none,identifier(none,i),integer_set(none)),member(none,identifier(none,i),interval(none,integer(none,1),integer(none,400))))))]),theorems(none,[]),sets(none,[])])],[exporter_version(3),po(sort_m2,'Well-definedness of Invariant',[invariant(inv3_m2)],true),po(sort_m2,'Invariant establishment',[event('INITIALISATION'),event('INITIALISATION'),invariant(inv1_m2)],true),po(sort_m2,'Invariant establishment',[event('INITIALISATION'),event('INITIALISATION'),invariant(inv2_m2)],true),po(sort_m2,'Invariant establishment',[event('INITIALISATION'),event('INITIALISATION'),invariant(inv3_m2)],true),po(sort_m2,'Action simulation',[event('INITIALISATION'),action(act3),event('INITIALISATION')],true),po(sort_m2,'Invariant preservation',[event(progress),event(progress),invariant(inv1_m2)],true),po(sort_m2,'Invariant preservation',[event(progress),event(progress),invariant(inv2_m2)],true),po(sort_m2,'Invariant preservation',[event(progress),event(progress),invariant(inv3_m2)],false),po(sort_m2,'Guard strengthening (split)',[event(progress),guard(grd2),event(progress),event(progress)],true),po(sort_m2,'Guard strengthening (split)',[event(progress),guard(grd3),event(progress),event(progress)],true),po(sort_m2,'Action simulation',[event(progress),action(act3),event(progress)],true),po(sort_m2,'Well-definedness of Guard',[guard(grd3),event(prog1)],true),po(sort_m2,'Invariant preservation',[event(prog),event(prog1),invariant(inv1_m2)],true),po(sort_m2,'Invariant preservation',[event(prog),event(prog1),invariant(inv2_m2)],true),po(sort_m2,'Invariant preservation',[event(prog),event(prog1),invariant(inv3_m2)],false),po(sort_m2,'Action simulation',[event(prog),action(act1),event(prog1)],true),po(sort_m2,'Variant of event',[variant(sort_m2),event(prog1)],true),po(sort_m2,'Natural number variant of event',[variant(sort_m2),event(prog1)],true),po(sort_m2,'Well-definedness of Guard',[guard(grd3),event(prog2)],true),po(sort_m2,'Invariant preservation',[event(prog),event(prog2),invariant(inv1_m2)],true),po(sort_m2,'Invariant preservation',[event(prog),event(prog2),invariant(inv2_m2)],true),po(sort_m2,'Invariant preservation',[event(prog),event(prog2),invariant(inv3_m2)],false),po(sort_m2,'Action simulation',[event(prog),action(act1),event(prog2)],true),po(sort_m2,'Variant of event',[variant(sort_m2),event(prog2)],true),po(sort_m2,'Natural number variant of event',[variant(sort_m2),event(prog2)],true),po(sort_m1,'Well-definedness of Invariant',[invariant(inv4_m1)],true),po(sort_m1,'Well-definedness of Theorem',[invariant(thm1_m1)],true),po(sort_m1,'Theorem',[invariant(thm1_m1)],true),po(sort_m1,'Well-definedness of Theorem',[invariant(thm2_m1)],true),po(sort_m1,'Theorem',[invariant(thm2_m1)],true),po(sort_m1,'Theorem',[invariant(thm3_m1)],true),po(sort_m1,'Well-definedness of Theorem',[invariant(thm4_m1)],true),po(sort_m1,'Theorem',[invariant(thm4_m1)],true),po(sort_m1,'Well-definedness of Theorem',[invariant(thm5_m1)],true),po(sort_m1,'Theorem',[invariant(thm5_m1)],true),po(sort_m1,'Well-definedness of Theorem',[invariant(thm6_m1)],true),po(sort_m1,'Theorem',[invariant(thm6_m1)],false),po(sort_m1,'Invariant establishment',[event('INITIALISATION'),event('INITIALISATION'),invariant(inv1_m1)],true),po(sort_m1,'Invariant establishment',[event('INITIALISATION'),event('INITIALISATION'),invariant(inv2_m1)],true),po(sort_m1,'Invariant establishment',[event('INITIALISATION'),event('INITIALISATION'),invariant(inv3_m1)],true),po(sort_m1,'Invariant establishment',[event('INITIALISATION'),event('INITIALISATION'),invariant(inv4_m1)],true),po(sort_m1,'Invariant establishment',[event('INITIALISATION'),event('INITIALISATION'),invariant(inv5_m1)],true),po(sort_m1,'Feasibility of action',[action(act3)],true),po(sort_m1,'Action simulation',[event('INITIALISATION'),action(act1),event('INITIALISATION')],true),po(sort_m1,'Well-definedness of Guard',[guard(grd3),event(progress)],true),po(sort_m1,'Invariant preservation',[event(progress),event(progress),invariant(inv1_m1)],true),po(sort_m1,'Invariant preservation',[event(progress),event(progress),invariant(inv2_m1)],false),po(sort_m1,'Invariant preservation',[event(progress),event(progress),invariant(inv3_m1)],true),po(sort_m1,'Invariant preservation',[event(progress),event(progress),invariant(inv4_m1)],false),po(sort_m1,'Invariant preservation',[event(progress),event(progress),invariant(inv5_m1)],true),po(sort_m1,'Well-definedness of action',[action(act1)],true),po(sort_m1,'Feasibility of action',[action(act3)],true),po(sort_m1,'Action simulation',[event(progress),action(act1),event(progress)],true),po(sort_m1,'Variant of event',[variant(sort_m1),event(progress)],true),po(sort_m1,'Natural number variant of event',[variant(sort_m1),event(progress)],true),po(sort_m1,'Invariant preservation',[event(prog),invariant(inv5_m1)],true),po(sort_m1,'Feasibility of action',[action(act1)],true),po(sort_m1,'Guard strengthening (split)',[event(final_evt),guard(grd1),event(final_evt),event(final_evt)],true),po(sort_m1,'Guard strengthening (split)',[event(final_evt),guard(grd2),event(final_evt),event(final_evt)],true),po(sort_m1,'Guard strengthening (split)',[event(final_evt),guard(grd3),event(final_evt),event(final_evt)],true),po(sort_m0,'Invariant establishment',[event('INITIALISATION'),invariant(inv1)],true),po(sort_m0,'Feasibility of action',[action(act1)],true),po(sort_m0,'Invariant preservation',[event(progress),invariant(inv1)],true),po(sort_m0,'Feasibility of action',[action(act1)],true),po(sort_m0,'Well-definedness of Guard',[guard(grd3),event(final_evt)],true)],_Error)).
2