1		package(load_event_b_project([event_b_model(none,f_m1,[sees(none,[f_c0,f_c1,f_c2]),refines(none,f_m0),variables(none,[identifier(none,now),identifier(none,phase),identifier(none,r),identifier(none,rho_c)]),invariant(none,[member(rodinpos(f_m1,inv1,'S'),identifier(none,now),natural_set(none)),member(rodinpos(f_m1,inv2,'U'),identifier(none,rho_c),total_function(none,natural_set(none),integer_set(none))),equal(rodinpos(f_m1,inv3,'V'),identifier(none,rho),function(none,identifier(none,rho_c),[identifier(none,now)])),implication(rodinpos(f_m1,inv4,'W'),member(none,identifier(none,phase),set_extension(none,[integer(none,0),integer(none,1)])),equal(none,identifier(none,now),integer(none,0))),implication(rodinpos(f_m1,inv5,'X'),equal(none,identifier(none,phase),integer(none,1)),less_equal(none,multiplication(none,identifier(none,r),identifier(none,sqrt3)),identifier(none,rhoi))),implication(rodinpos(f_m1,inv6,'Y'),equal(none,identifier(none,phase),integer(none,0)),equal(none,identifier(none,rho_c),event_b_comprehension_set(none,[identifier(none,t)],couple(none,[identifier(none,t),identifier(none,rhoi)]),conjunct(none,member(none,identifier(none,t),integer_set(none)),greater_equal(none,identifier(none,t),integer(none,0)))))),implication(rodinpos(f_m1,inv7,'Z'),equal(none,identifier(none,phase),integer(none,1)),equal(none,identifier(none,rho_c),event_b_comprehension_set(none,[identifier(none,t)],couple(none,[identifier(none,t),identifier(none,rhoi)]),conjunct(none,member(none,identifier(none,t),integer_set(none)),greater_equal(none,identifier(none,t),integer(none,0)))))),implication(rodinpos(f_m1,inv8,'['),equal(none,identifier(none,phase),integer(none,3)),forall(none,[identifier(none,t)],implication(none,conjunct(none,member(none,identifier(none,t),integer_set(none)),greater_equal(none,identifier(none,t),identifier(none,now))),equal(none,function(none,identifier(none,rho_c),[identifier(none,t)]),multiplication(none,identifier(none,r),function(none,identifier(none,sqrt),[minus(none,integer(none,5),multiplication(none,integer(none,4),function(none,identifier(none,cos),[minus(none,div(none,identifier(none,pi),integer(none,3)),div(none,multiplication(none,identifier(none,v),add(none,minus(none,identifier(none,t),identifier(none,now)),div(none,multiplication(none,identifier(none,pi),identifier(none,r)),multiplication(none,integer(none,3),identifier(none,v))))),identifier(none,r)))])))]))))))]),theorems(none,[]),events(none,[event(rodinpos(f_m1,'INITIALISATION','\''),'INITIALISATION',ordinary(none),['INITIALISATION'],[],[],[],[assign(rodinpos(f_m1,act5,'+'),[identifier(none,phase)],[integer(none,0)]),assign(rodinpos(f_m1,act6,','),[identifier(none,r)],[integer(none,1)]),assign(rodinpos(f_m1,act8,'\''),[identifier(none,now)],[integer(none,0)]),assign(rodinpos(f_m1,act9,'('),[identifier(none,rho_c)],[event_b_comprehension_set(none,[identifier(none,t)],couple(none,[identifier(none,t),identifier(none,rhoi)]),conjunct(none,member(none,identifier(none,t),integer_set(none)),greater_equal(none,identifier(none,t),integer(none,0))))])],[]),event(rodinpos(f_m1,agree,'Q'),agree,ordinary(none),[agree],[identifier(rodinpos(f_m1,[],'\''),c)],[equal(rodinpos(f_m1,grd1,'*'),identifier(none,phase),integer(none,0)),greater(rodinpos(f_m1,grd2,','),identifier(none,c),integer(none,0)),less_equal(rodinpos(f_m1,grd3,'('),identifier(none,p),multiplication(none,integer(none,2),multiplication(none,identifier(none,c),identifier(none,sin_phi_d_2)))),less_equal(rodinpos(f_m1,grd4,'-'),multiplication(none,identifier(none,c),identifier(none,sqrt3)),identifier(none,rhoi))],[],[assign(rodinpos(f_m1,act1,'+'),[identifier(none,phase)],[integer(none,1)]),assign(rodinpos(f_m1,act2,')'),[identifier(none,r)],[identifier(none,c)])],[]),event(rodinpos(f_m1,start,'7'),start,ordinary(none),[start],[],[equal(rodinpos(f_m1,grd1,'\''),identifier(none,phase),integer(none,1))],[],[assign(rodinpos(f_m1,act1,'('),[identifier(none,phase)],[integer(none,2)]),assign(rodinpos(f_m1,act5,','),[identifier(none,rho_c)],[overwrite(none,identifier(none,rho_c),event_b_comprehension_set(none,[identifier(none,t)],couple(none,[identifier(none,t),minus(none,identifier(none,rhoi),multiplication(none,identifier(none,v),minus(none,identifier(none,t),identifier(none,now))))]),conjunct(none,member(none,identifier(none,t),integer_set(none)),greater_equal(none,identifier(none,t),identifier(none,now)))))]),assign(rodinpos(f_m1,act6,'-'),[identifier(none,now)],[add(none,identifier(none,now),div(none,minus(none,identifier(none,rhoi),multiplication(none,identifier(none,sqrt3),identifier(none,r))),identifier(none,v)))])],[]),event(rodinpos(f_m1,turning_1,'8'),turning_1,ordinary(none),[turning_1],[],[equal(rodinpos(f_m1,grd1,'\''),identifier(none,phase),integer(none,2))],[],[assign(rodinpos(f_m1,act1,'('),[identifier(none,phase)],[integer(none,3)]),assign(rodinpos(f_m1,act7,'.'),[identifier(none,now)],[add(none,identifier(none,now),div(none,multiplication(none,identifier(none,pi),identifier(none,r)),multiplication(none,integer(none,3),identifier(none,v))))]),assign(rodinpos(f_m1,act8,'/'),[identifier(none,rho_c)],[overwrite(none,identifier(none,rho_c),event_b_comprehension_set(none,[identifier(none,t)],couple(none,[identifier(none,t),multiplication(none,identifier(none,r),function(none,identifier(none,sqrt),[minus(none,integer(none,5),multiplication(none,integer(none,4),function(none,identifier(none,cos),[minus(none,div(none,identifier(none,pi),integer(none,3)),div(none,multiplication(none,identifier(none,v),minus(none,identifier(none,t),identifier(none,now))),identifier(none,r)))])))]))]),conjunct(none,member(none,identifier(none,t),integer_set(none)),greater_equal(none,identifier(none,t),identifier(none,now)))))])],[]),event(rodinpos(f_m1,cycling,'E'),cycling,ordinary(none),[cycling],[],[equal(rodinpos(f_m1,grd1,'\''),identifier(none,phase),integer(none,3))],[],[assign(rodinpos(f_m1,act1,'('),[identifier(none,phase)],[integer(none,4)]),assign(rodinpos(f_m1,act5,','),[identifier(none,now)],[add(none,identifier(none,now),div(none,multiplication(none,integer(none,2),multiplication(none,identifier(none,pi),identifier(none,r))),multiplication(none,integer(none,3),identifier(none,v))))]),assign(rodinpos(f_m1,act6,'-'),[identifier(none,rho_c)],[overwrite(none,identifier(none,rho_c),event_b_comprehension_set(none,[identifier(none,t)],couple(none,[identifier(none,t),identifier(none,r)]),conjunct(none,member(none,identifier(none,t),integer_set(none)),greater_equal(none,identifier(none,t),identifier(none,now)))))])],[]),event(rodinpos(f_m1,turning_2,'F'),turning_2,ordinary(none),[turning_2],[],[equal(rodinpos(f_m1,grd1,'\''),identifier(none,phase),integer(none,4))],[],[assign(rodinpos(f_m1,act1,'('),[identifier(none,phase)],[integer(none,5)]),assign(rodinpos(f_m1,act7,'.'),[identifier(none,now)],[add(none,identifier(none,now),div(none,multiplication(none,identifier(none,pi),identifier(none,r)),multiplication(none,integer(none,3),identifier(none,v))))]),assign(rodinpos(f_m1,act8,'/'),[identifier(none,rho_c)],[overwrite(none,identifier(none,rho_c),event_b_comprehension_set(none,[identifier(none,t)],couple(none,[identifier(none,t),multiplication(none,identifier(none,r),function(none,identifier(none,sqrt),[minus(none,integer(none,5),multiplication(none,integer(none,4),function(none,identifier(none,cos),[div(none,multiplication(none,identifier(none,v),minus(none,identifier(none,t),identifier(none,now))),identifier(none,r))])))]))]),conjunct(none,member(none,identifier(none,t),integer_set(none)),greater_equal(none,identifier(none,t),identifier(none,now)))))])],[])])]),event_b_model(none,f_m0,[sees(none,[f_c0]),variables(none,[identifier(none,phase),identifier(none,r),identifier(none,rho)]),invariant(none,[greater(rodinpos(f_m0,inv1,')'),identifier(none,rho),integer(none,0)),greater(rodinpos(f_m0,inv3,'R'),identifier(none,r),integer(none,0)),greater_equal(rodinpos(f_m0,inv5,'P'),multiplication(none,integer(none,2),multiplication(none,identifier(none,rho),identifier(none,sin_phi_d_2))),identifier(none,p)),implication(rodinpos(f_m0,inv6,'U'),not_equal(none,identifier(none,phase),integer(none,0)),greater_equal(none,multiplication(none,integer(none,2),multiplication(none,identifier(none,r),identifier(none,sin_phi_d_2))),identifier(none,p))),implication(rodinpos(f_m0,inv7,'X'),equal(none,identifier(none,phase),integer(none,1)),member(none,minus(none,identifier(none,rhoi),multiplication(none,identifier(none,sqrt3),identifier(none,r))),natural_set(none)))]),theorems(none,[]),events(none,[event(rodinpos(f_m0,'INITIALISATION','\''),'INITIALISATION',ordinary(none),[],[],[],[],[assign(rodinpos(f_m0,act1,'\''),[identifier(none,rho)],[identifier(none,rhoi)]),assign(rodinpos(f_m0,act2,'+'),[identifier(none,phase)],[integer(none,0)]),assign(rodinpos(f_m0,act3,','),[identifier(none,r)],[integer(none,1)])],[]),event(rodinpos(f_m0,agree,'Q'),agree,ordinary(none),[],[identifier(rodinpos(f_m0,[],'\''),c)],[equal(rodinpos(f_m0,grd1,'*'),identifier(none,phase),integer(none,0)),greater(rodinpos(f_m0,grd2,','),identifier(none,c),integer(none,0)),less_equal(rodinpos(f_m0,grd3,'('),identifier(none,p),multiplication(none,integer(none,2),multiplication(none,identifier(none,c),identifier(none,sin_phi_d_2)))),less_equal(rodinpos(f_m0,grd4,'-'),multiplication(none,identifier(none,c),identifier(none,sqrt3)),identifier(none,rhoi))],[],[assign(rodinpos(f_m0,act1,'+'),[identifier(none,phase)],[integer(none,1)]),assign(rodinpos(f_m0,act2,')'),[identifier(none,r)],[identifier(none,c)])],[]),event(rodinpos(f_m0,start,'7'),start,ordinary(none),[],[],[equal(rodinpos(f_m0,grd1,'\''),identifier(none,phase),integer(none,1))],[],[assign(rodinpos(f_m0,act1,'('),[identifier(none,phase)],[integer(none,2)]),assign(rodinpos(f_m0,act2,')'),[identifier(none,rho)],[multiplication(none,identifier(none,sqrt3),identifier(none,r))])],[]),event(rodinpos(f_m0,turning_1,'8'),turning_1,ordinary(none),[],[],[equal(rodinpos(f_m0,grd1,'\''),identifier(none,phase),integer(none,2))],[],[assign(rodinpos(f_m0,act1,'('),[identifier(none,phase)],[integer(none,3)]),assign(rodinpos(f_m0,act3,'+'),[identifier(none,rho)],[identifier(none,r)])],[]),event(rodinpos(f_m0,cycling,'E'),cycling,ordinary(none),[],[],[equal(rodinpos(f_m0,grd1,'\''),identifier(none,phase),integer(none,3))],[],[assign(rodinpos(f_m0,act1,'('),[identifier(none,phase)],[integer(none,4)])],[]),event(rodinpos(f_m0,turning_2,'F'),turning_2,ordinary(none),[],[],[equal(rodinpos(f_m0,grd1,'\''),identifier(none,phase),integer(none,4))],[],[assign(rodinpos(f_m0,act1,'('),[identifier(none,phase)],[integer(none,5)]),assign(rodinpos(f_m0,act3,'+'),[identifier(none,rho)],[multiplication(none,identifier(none,r),identifier(none,sqrt3))])],[])])])],[event_b_context(none,f_c0,[extends(none,[]),constants(none,[identifier(none,p),identifier(none,pi),identifier(none,rhoi),identifier(none,sin_phi_d_2),identifier(none,sqrt3)]),abstract_constants(none,[]),axioms(none,[greater(rodinpos(f_c0,axm1,'('),identifier(none,rhoi),integer(none,0)),greater(rodinpos(f_c0,axm7,'9'),identifier(none,p),integer(none,0)),greater(rodinpos(f_c0,axm6,'8'),identifier(none,sin_phi_d_2),integer(none,0)),greater_equal(rodinpos(f_c0,axm5,'6'),multiplication(none,integer(none,2),multiplication(none,identifier(none,rhoi),identifier(none,sin_phi_d_2))),multiplication(none,identifier(none,p),identifier(none,sqrt3))),greater(rodinpos(f_c0,axm8,';'),identifier(none,sqrt3),integer(none,0)),equal(rodinpos(f_c0,axm9,'='),multiplication(none,identifier(none,sqrt3),identifier(none,sqrt3)),integer(none,3)),greater(rodinpos(f_c0,axm10,'?'),identifier(none,pi),integer(none,0))]),theorems(none,[]),sets(none,[])]),event_b_context(none,f_c1,[extends(none,[f_c0]),constants(none,[identifier(none,v)]),abstract_constants(none,[]),axioms(none,[greater(rodinpos(f_c1,axm1,')'),identifier(none,v),integer(none,0)),forall(rodinpos(f_c1,axm4,','),[identifier(none,x)],implication(none,member(none,identifier(none,x),integer_set(none)),equal(none,multiplication(none,identifier(none,v),div(none,identifier(none,x),identifier(none,v))),identifier(none,x)))),forall(rodinpos(f_c1,axm5,'-'),[identifier(none,x)],implication(none,conjunct(none,member(none,identifier(none,x),integer_set(none)),greater(none,identifier(none,x),integer(none,0))),greater(none,div(none,identifier(none,x),identifier(none,v)),integer(none,0)))),forall(rodinpos(f_c1,axm6,'.'),[identifier(none,x),identifier(none,y)],implication(none,conjunct(none,member(none,identifier(none,x),integer_set(none)),conjunct(none,member(none,identifier(none,y),integer_set(none)),conjunct(none,greater(none,identifier(none,x),integer(none,0)),greater(none,identifier(none,y),integer(none,0))))),greater(none,div(none,identifier(none,x),identifier(none,y)),integer(none,0)))),forall(rodinpos(f_c1,axm7,'/'),[identifier(none,x)],implication(none,conjunct(none,member(none,identifier(none,x),integer_set(none)),greater_equal(none,identifier(none,x),integer(none,0))),greater_equal(none,div(none,identifier(none,x),identifier(none,v)),integer(none,0)))),greater(rodinpos(f_c1,axm8,'0'),multiplication(none,integer(none,3),identifier(none,v)),integer(none,0)),forall(rodinpos(f_c1,axm9,'1'),[identifier(none,x)],implication(none,conjunct(none,member(none,identifier(none,x),integer_set(none)),greater_equal(none,identifier(none,x),integer(none,0))),greater_equal(none,div(none,identifier(none,x),multiplication(none,integer(none,3),identifier(none,v))),integer(none,0)))),forall(rodinpos(f_c1,axm10,'2'),[identifier(none,x)],implication(none,conjunct(none,member(none,identifier(none,x),integer_set(none)),greater(none,identifier(none,x),integer(none,0))),equal(none,div(none,multiplication(none,identifier(none,v),div(none,multiplication(none,identifier(none,pi),identifier(none,x)),multiplication(none,integer(none,3),identifier(none,v)))),identifier(none,x)),div(none,identifier(none,pi),integer(none,3)))))]),theorems(none,[]),sets(none,[])]),event_b_context(none,f_c2,[extends(none,[f_c1]),constants(none,[identifier(none,cos),identifier(none,sqrt)]),abstract_constants(none,[]),axioms(none,[member(rodinpos(f_c2,axm1,')'),identifier(none,sqrt),total_function(none,natural_set(none),natural_set(none))),member(rodinpos(f_c2,axm2,'+'),identifier(none,cos),total_function(none,integer_set(none),interval(none,integer(none,-1),integer(none,1)))),forall(rodinpos(f_c2,axm3,','),[identifier(none,x),identifier(none,y),identifier(none,z)],implication(none,conjunct(none,member(none,identifier(none,x),integer_set(none)),conjunct(none,member(none,identifier(none,y),integer_set(none)),conjunct(none,member(none,identifier(none,z),integer_set(none)),conjunct(none,member(none,identifier(none,x),natural_set(none)),conjunct(none,greater(none,identifier(none,y),integer(none,0)),greater(none,identifier(none,z),integer(none,0))))))),equal(none,div(none,div(none,multiplication(none,identifier(none,x),identifier(none,y)),identifier(none,z)),identifier(none,y)),div(none,identifier(none,x),identifier(none,z))))),equal(rodinpos(f_c2,axm4,'-'),function(none,identifier(none,cos),[integer(none,0)]),integer(none,1)),equal(rodinpos(f_c2,axm5,'.'),function(none,identifier(none,sqrt),[integer(none,1)]),integer(none,1)),equal(rodinpos(f_c2,axm6,'/'),multiplication(none,integer(none,4),function(none,identifier(none,cos),[div(none,identifier(none,pi),integer(none,3))])),integer(none,2)),equal(rodinpos(f_c2,axm7,'0'),identifier(none,sqrt3),function(none,identifier(none,sqrt),[integer(none,3)])),forall(rodinpos(f_c2,axm8,'1'),[identifier(none,a),identifier(none,b),identifier(none,c)],implication(none,conjunct(none,member(none,identifier(none,a),integer_set(none)),conjunct(none,member(none,identifier(none,b),integer_set(none)),conjunct(none,member(none,identifier(none,c),integer_set(none)),conjunct(none,greater(none,identifier(none,c),integer(none,0)),greater(none,identifier(none,b),integer(none,0)))))),equal(none,div(none,multiplication(none,identifier(none,v),div(none,div(none,multiplication(none,identifier(none,a),identifier(none,b)),identifier(none,c)),identifier(none,v))),identifier(none,b)),div(none,identifier(none,a),identifier(none,c)))))]),theorems(none,[]),sets(none,[])])],[exporter_version(3),po(f_c1,'Well-definedness of Axiom',[axiom(axm4)],true),po(f_c1,'Well-definedness of Axiom',[axiom(axm5)],true),po(f_c1,'Well-definedness of Axiom',[axiom(axm6)],true),po(f_c1,'Well-definedness of Axiom',[axiom(axm7)],true),po(f_c1,'Well-definedness of Axiom',[axiom(axm9)],true),po(f_c1,'Well-definedness of Axiom',[axiom(axm10)],true),po(f_c2,'Well-definedness of Axiom',[axiom(axm3)],true),po(f_c2,'Well-definedness of Axiom',[axiom(axm4)],true),po(f_c2,'Well-definedness of Axiom',[axiom(axm5)],true),po(f_c2,'Well-definedness of Axiom',[axiom(axm6)],true),po(f_c2,'Well-definedness of Axiom',[axiom(axm7)],true),po(f_c2,'Well-definedness of Axiom',[axiom(axm8)],true),po(f_m1,'Well-definedness of Invariant',[invariant(inv3)],true),po(f_m1,'Well-definedness of Invariant',[invariant(inv8)],true),po(f_m1,'Invariant establishment',[event('INITIALISATION'),event('INITIALISATION'),invariant(inv1)],false),po(f_m1,'Invariant establishment',[event('INITIALISATION'),event('INITIALISATION'),invariant(inv2)],true),po(f_m1,'Invariant establishment',[event('INITIALISATION'),event('INITIALISATION'),invariant(inv3)],false),po(f_m1,'Invariant establishment',[event('INITIALISATION'),event('INITIALISATION'),invariant(inv4)],false),po(f_m1,'Invariant establishment',[event('INITIALISATION'),event('INITIALISATION'),invariant(inv5)],false),po(f_m1,'Invariant establishment',[event('INITIALISATION'),event('INITIALISATION'),invariant(inv6)],false),po(f_m1,'Invariant establishment',[event('INITIALISATION'),event('INITIALISATION'),invariant(inv7)],false),po(f_m1,'Invariant establishment',[event('INITIALISATION'),event('INITIALISATION'),invariant(inv8)],false),po(f_m1,'Action simulation',[event('INITIALISATION'),action(act2),event('INITIALISATION')],false),po(f_m1,'Invariant preservation',[event(agree),event(agree),invariant(inv4)],false),po(f_m1,'Invariant preservation',[event(agree),event(agree),invariant(inv5)],true),po(f_m1,'Invariant preservation',[event(agree),event(agree),invariant(inv6)],true),po(f_m1,'Invariant preservation',[event(agree),event(agree),invariant(inv7)],true),po(f_m1,'Invariant preservation',[event(agree),event(agree),invariant(inv8)],false),po(f_m1,'Invariant preservation',[event(start),event(start),invariant(inv1)],false),po(f_m1,'Invariant preservation',[event(start),event(start),invariant(inv2)],false),po(f_m1,'Invariant preservation',[event(start),event(start),invariant(inv3)],false),po(f_m1,'Invariant preservation',[event(start),event(start),invariant(inv4)],false),po(f_m1,'Invariant preservation',[event(start),event(start),invariant(inv5)],true),po(f_m1,'Invariant preservation',[event(start),event(start),invariant(inv6)],false),po(f_m1,'Invariant preservation',[event(start),event(start),invariant(inv7)],false),po(f_m1,'Invariant preservation',[event(start),event(start),invariant(inv8)],false),po(f_m1,'Well-definedness of action',[action(act6)],false),po(f_m1,'Invariant preservation',[event(turning_1),event(turning_1),invariant(inv1)],false),po(f_m1,'Invariant preservation',[event(turning_1),event(turning_1),invariant(inv2)],false),po(f_m1,'Invariant preservation',[event(turning_1),event(turning_1),invariant(inv3)],false),po(f_m1,'Invariant preservation',[event(turning_1),event(turning_1),invariant(inv4)],false),po(f_m1,'Invariant preservation',[event(turning_1),event(turning_1),invariant(inv5)],false),po(f_m1,'Invariant preservation',[event(turning_1),event(turning_1),invariant(inv6)],false),po(f_m1,'Invariant preservation',[event(turning_1),event(turning_1),invariant(inv7)],false),po(f_m1,'Invariant preservation',[event(turning_1),event(turning_1),invariant(inv8)],false),po(f_m1,'Well-definedness of action',[action(act7)],false),po(f_m1,'Well-definedness of action',[action(act8)],false),po(f_m1,'Invariant preservation',[event(cycling),event(cycling),invariant(inv1)],true),po(f_m1,'Invariant preservation',[event(cycling),event(cycling),invariant(inv2)],true),po(f_m1,'Invariant preservation',[event(cycling),event(cycling),invariant(inv3)],true),po(f_m1,'Invariant preservation',[event(cycling),event(cycling),invariant(inv4)],true),po(f_m1,'Invariant preservation',[event(cycling),event(cycling),invariant(inv5)],true),po(f_m1,'Invariant preservation',[event(cycling),event(cycling),invariant(inv6)],true),po(f_m1,'Invariant preservation',[event(cycling),event(cycling),invariant(inv7)],true),po(f_m1,'Invariant preservation',[event(cycling),event(cycling),invariant(inv8)],true),po(f_m1,'Well-definedness of action',[action(act5)],true),po(f_m1,'Invariant preservation',[event(turning_2),event(turning_2),invariant(inv1)],false),po(f_m1,'Invariant preservation',[event(turning_2),event(turning_2),invariant(inv2)],false),po(f_m1,'Invariant preservation',[event(turning_2),event(turning_2),invariant(inv3)],false),po(f_m1,'Invariant preservation',[event(turning_2),event(turning_2),invariant(inv4)],false),po(f_m1,'Invariant preservation',[event(turning_2),event(turning_2),invariant(inv5)],false),po(f_m1,'Invariant preservation',[event(turning_2),event(turning_2),invariant(inv6)],false),po(f_m1,'Invariant preservation',[event(turning_2),event(turning_2),invariant(inv7)],false),po(f_m1,'Invariant preservation',[event(turning_2),event(turning_2),invariant(inv8)],false),po(f_m1,'Well-definedness of action',[action(act7)],false),po(f_m1,'Well-definedness of action',[action(act8)],false),po(f_m0,'Invariant establishment',[event('INITIALISATION'),invariant(inv1)],true),po(f_m0,'Invariant establishment',[event('INITIALISATION'),invariant(inv3)],false),po(f_m0,'Invariant establishment',[event('INITIALISATION'),invariant(inv5)],true),po(f_m0,'Invariant establishment',[event('INITIALISATION'),invariant(inv6)],false),po(f_m0,'Invariant establishment',[event('INITIALISATION'),invariant(inv7)],false),po(f_m0,'Invariant preservation',[event(agree),invariant(inv3)],true),po(f_m0,'Invariant preservation',[event(agree),invariant(inv6)],false),po(f_m0,'Invariant preservation',[event(agree),invariant(inv7)],false),po(f_m0,'Invariant preservation',[event(start),invariant(inv1)],false),po(f_m0,'Invariant preservation',[event(start),invariant(inv5)],false),po(f_m0,'Invariant preservation',[event(start),invariant(inv6)],false),po(f_m0,'Invariant preservation',[event(start),invariant(inv7)],true),po(f_m0,'Invariant preservation',[event(turning_1),invariant(inv1)],true),po(f_m0,'Invariant preservation',[event(turning_1),invariant(inv5)],false),po(f_m0,'Invariant preservation',[event(turning_1),invariant(inv6)],false),po(f_m0,'Invariant preservation',[event(turning_1),invariant(inv7)],false),po(f_m0,'Invariant preservation',[event(cycling),invariant(inv6)],true),po(f_m0,'Invariant preservation',[event(cycling),invariant(inv7)],true),po(f_m0,'Invariant preservation',[event(turning_2),invariant(inv1)],false),po(f_m0,'Invariant preservation',[event(turning_2),invariant(inv5)],false),po(f_m0,'Invariant preservation',[event(turning_2),invariant(inv6)],false),po(f_m0,'Invariant preservation',[event(turning_2),invariant(inv7)],false)],_Error)).
2