package(load_event_b_project([event_b_model(none,'C_m3_prob',[sees(none,['C_c0','C_c1','C_c0_prob','C_c1_prob']),refines(none,'C_m3'),variables(none,[identifier(none,state),identifier(none,'TT'),identifier(none,t2_c),identifier(none,temp),identifier(none,new_now),identifier(none,t1_c)]),invariant(none,[]),theorems(none,[]),events(none,[event(rodinpos('C_m3_prob','INITIALISATION','K'),'INITIALISATION',ordinary(none),['INITIALISATION'],[],[],[],[assign(rodinpos('C_m3_prob',act1,internal1),[identifier(none,t1_c)],[event_b_comprehension_set(none,[identifier(none,t)],couple(none,[identifier(none,t),add(none,multiplication(none,integer(none,2),identifier(none,a)),identifier(none,b2))]),conjunct(none,[member(none,identifier(none,t),integer_set(none)),member(none,identifier(none,t),natural_set(none))]))]),assign(rodinpos('C_m3_prob',act2,internal2),[identifier(none,t2_c)],[event_b_comprehension_set(none,[identifier(none,t)],couple(none,[identifier(none,t),identifier(none,a)]),conjunct(none,[member(none,identifier(none,t),integer_set(none)),member(none,identifier(none,t),natural_set(none))]))]),assign(rodinpos('C_m3_prob',act3,')'),[identifier(none,state)],[integer(none,0)]),assign(rodinpos('C_m3_prob',act7,internal4),[identifier(none,temp)],[event_b_comprehension_set(none,[identifier(none,t)],couple(none,[identifier(none,t),identifier(none,tM)]),conjunct(none,[member(none,identifier(none,t),integer_set(none)),member(none,identifier(none,t),natural_set(none))]))]),assign(rodinpos('C_m3_prob',act8,'\''),[identifier(none,'TT')],[boolean_false(none)]),assign(rodinpos('C_m3_prob',act9,'('),[identifier(none,new_now)],[integer(none,0)])],[]),event(rodinpos('C_m3_prob',cool_rod1,'L'),cool_rod1,ordinary(none),[cool_rod1],[],[equal(rodinpos('C_m3_prob',grd1,'\''),identifier(none,state),integer(none,0)),greater_equal(rodinpos('C_m3_prob',grd2,'('),function(none,identifier(none,t1_c),[identifier(none,new_now)]),identifier(none,'T')),equal(rodinpos('C_m3_prob',grd5,'2'),identifier(none,'TT'),boolean_false(none))],[equal(rodinpos('C_m3_prob',grd3,'/'),function(none,identifier(none,temp),[identifier(none,new_now)]),identifier(none,tM)),member(rodinpos('C_m3_prob',grd4,'1'),identifier(none,b1),natural_set(none))],[assign(rodinpos('C_m3_prob',act1,')'),[identifier(none,state)],[integer(none,1)]),assign(rodinpos('C_m3_prob',act3,'+'),[identifier(none,t2_c)],[overwrite(none,identifier(none,t2_c),event_b_comprehension_set(none,[identifier(none,t)],couple(none,[identifier(none,t),add(none,function(none,identifier(none,t2_c),[identifier(none,new_now)]),minus(none,identifier(none,t),identifier(none,new_now)))]),conjunct(none,[member(none,identifier(none,t),integer_set(none)),greater_equal(none,identifier(none,t),identifier(none,new_now))])))]),assign(rodinpos('C_m3_prob',act4,'3'),[identifier(none,'TT')],[boolean_true(none)]),assign(rodinpos('C_m3_prob',act5,'.'),[identifier(none,t1_c)],[overwrite(none,identifier(none,t1_c),event_b_comprehension_set(none,[identifier(none,t)],couple(none,[identifier(none,t),function(none,identifier(none,t1_c),[identifier(none,new_now)])]),conjunct(none,[member(none,identifier(none,t),integer_set(none)),greater_equal(none,identifier(none,t),identifier(none,new_now))])))]),assign(rodinpos('C_m3_prob',act6,'0'),[identifier(none,temp)],[overwrite(none,identifier(none,temp),event_b_comprehension_set(none,[identifier(none,t)],couple(none,[identifier(none,t),minus(none,identifier(none,tM),multiplication(none,identifier(none,v1),minus(none,identifier(none,t),identifier(none,new_now))))]),conjunct(none,[member(none,identifier(none,t),integer_set(none)),greater_equal(none,identifier(none,t),identifier(none,new_now))])))])],[]),event(rodinpos('C_m3_prob',cool_rod2,'M'),cool_rod2,ordinary(none),[cool_rod2],[],[equal(rodinpos('C_m3_prob',grd1,'\''),identifier(none,state),integer(none,0)),greater_equal(rodinpos('C_m3_prob',grd2,'('),function(none,identifier(none,t2_c),[identifier(none,new_now)]),identifier(none,'T')),equal(rodinpos('C_m3_prob',grd5,'2'),identifier(none,'TT'),boolean_false(none))],[equal(rodinpos('C_m3_prob',grd3,'/'),function(none,identifier(none,temp),[identifier(none,new_now)]),identifier(none,tM)),member(rodinpos('C_m3_prob',grd4,'1'),identifier(none,b2),natural_set(none))],[assign(rodinpos('C_m3_prob',act1,')'),[identifier(none,state)],[integer(none,2)]),assign(rodinpos('C_m3_prob',act3,'+'),[identifier(none,t1_c)],[overwrite(none,identifier(none,t1_c),event_b_comprehension_set(none,[identifier(none,t)],couple(none,[identifier(none,t),add(none,function(none,identifier(none,t1_c),[identifier(none,new_now)]),minus(none,identifier(none,t),identifier(none,new_now)))]),conjunct(none,[member(none,identifier(none,t),integer_set(none)),greater_equal(none,identifier(none,t),identifier(none,new_now))])))]),assign(rodinpos('C_m3_prob',act4,'-'),[identifier(none,'TT')],[boolean_true(none)]),assign(rodinpos('C_m3_prob',act5,'.'),[identifier(none,t2_c)],[overwrite(none,identifier(none,t2_c),event_b_comprehension_set(none,[identifier(none,t)],couple(none,[identifier(none,t),function(none,identifier(none,t2_c),[identifier(none,new_now)])]),conjunct(none,[member(none,identifier(none,t),integer_set(none)),greater_equal(none,identifier(none,t),identifier(none,new_now))])))]),assign(rodinpos('C_m3_prob',act6,'0'),[identifier(none,temp)],[overwrite(none,identifier(none,temp),event_b_comprehension_set(none,[identifier(none,t)],couple(none,[identifier(none,t),minus(none,identifier(none,tM),multiplication(none,identifier(none,v2),minus(none,identifier(none,t),identifier(none,new_now))))]),conjunct(none,[member(none,identifier(none,t),integer_set(none)),greater_equal(none,identifier(none,t),identifier(none,new_now))])))])],[]),event(rodinpos('C_m3_prob',release_rod1,'N'),release_rod1,ordinary(none),[release_rod1],[],[equal(rodinpos('C_m3_prob',grd1,'\''),identifier(none,state),integer(none,1)),equal(rodinpos('C_m3_prob',grd4,'0'),identifier(none,'TT'),boolean_false(none))],[equal(rodinpos('C_m3_prob',grd2,'-'),function(none,identifier(none,temp),[identifier(none,new_now)]),identifier(none,tm)),member(rodinpos('C_m3_prob',grd3,'/'),identifier(none,a),natural_set(none))],[assign(rodinpos('C_m3_prob',act1,'('),[identifier(none,state)],[integer(none,0)]),assign(rodinpos('C_m3_prob',act2,')'),[identifier(none,t1_c)],[overwrite(none,identifier(none,t1_c),event_b_comprehension_set(none,[identifier(none,t)],couple(none,[identifier(none,t),minus(none,identifier(none,t),identifier(none,new_now))]),conjunct(none,[member(none,identifier(none,t),integer_set(none)),greater_equal(none,identifier(none,t),identifier(none,new_now))])))]),assign(rodinpos('C_m3_prob',act3,'*'),[identifier(none,t2_c)],[overwrite(none,identifier(none,t2_c),event_b_comprehension_set(none,[identifier(none,t)],couple(none,[identifier(none,t),add(none,function(none,identifier(none,t2_c),[identifier(none,new_now)]),minus(none,identifier(none,t),identifier(none,new_now)))]),conjunct(none,[member(none,identifier(none,t),integer_set(none)),greater_equal(none,identifier(none,t),identifier(none,new_now))])))]),assign(rodinpos('C_m3_prob',act4,','),[identifier(none,'TT')],[boolean_true(none)]),assign(rodinpos('C_m3_prob',act5,'.'),[identifier(none,temp)],[overwrite(none,identifier(none,temp),event_b_comprehension_set(none,[identifier(none,t)],couple(none,[identifier(none,t),add(none,identifier(none,tm),multiplication(none,identifier(none,vr),minus(none,identifier(none,t),identifier(none,new_now))))]),conjunct(none,[member(none,identifier(none,t),integer_set(none)),greater_equal(none,identifier(none,t),identifier(none,new_now))])))])],[]),event(rodinpos('C_m3_prob',release_rod2,'O'),release_rod2,ordinary(none),[release_rod2],[],[equal(rodinpos('C_m3_prob',grd1,'\''),identifier(none,state),integer(none,2)),equal(rodinpos('C_m3_prob',grd4,'/'),identifier(none,'TT'),boolean_false(none))],[equal(rodinpos('C_m3_prob',grd2,','),function(none,identifier(none,temp),[identifier(none,new_now)]),identifier(none,tm)),member(rodinpos('C_m3_prob',grd3,'.'),identifier(none,a),natural_set(none))],[assign(rodinpos('C_m3_prob',act1,'('),[identifier(none,state)],[integer(none,0)]),assign(rodinpos('C_m3_prob',act2,')'),[identifier(none,t1_c)],[overwrite(none,identifier(none,t1_c),event_b_comprehension_set(none,[identifier(none,t)],couple(none,[identifier(none,t),add(none,function(none,identifier(none,t1_c),[identifier(none,new_now)]),minus(none,identifier(none,t),identifier(none,new_now)))]),conjunct(none,[member(none,identifier(none,t),integer_set(none)),greater_equal(none,identifier(none,t),identifier(none,new_now))])))]),assign(rodinpos('C_m3_prob',act3,'*'),[identifier(none,t2_c)],[overwrite(none,identifier(none,t2_c),event_b_comprehension_set(none,[identifier(none,t)],couple(none,[identifier(none,t),minus(none,identifier(none,t),identifier(none,new_now))]),conjunct(none,[member(none,identifier(none,t),integer_set(none)),greater_equal(none,identifier(none,t),identifier(none,new_now))])))]),assign(rodinpos('C_m3_prob',act4,'+'),[identifier(none,'TT')],[boolean_true(none)]),assign(rodinpos('C_m3_prob',act5,'-'),[identifier(none,temp)],[overwrite(none,identifier(none,temp),event_b_comprehension_set(none,[identifier(none,t)],couple(none,[identifier(none,t),add(none,identifier(none,tm),multiplication(none,identifier(none,vr),minus(none,identifier(none,t),identifier(none,new_now))))]),conjunct(none,[member(none,identifier(none,t),integer_set(none)),greater_equal(none,identifier(none,t),identifier(none,new_now))])))])],[]),event(rodinpos('C_m3_prob','TIME_1','P'),'TIME_1',ordinary(none),['TIME_1'],[],[equal(rodinpos('C_m3_prob',grd1,'\''),identifier(none,state),integer(none,1)),equal(rodinpos('C_m3_prob',grd2,'('),identifier(none,'TT'),boolean_true(none))],[],[assign(rodinpos('C_m3_prob',act1,')'),[identifier(none,new_now)],[add(none,identifier(none,new_now),identifier(none,b1))]),assign(rodinpos('C_m3_prob',act2,'*'),[identifier(none,'TT')],[boolean_false(none)])],[]),event(rodinpos('C_m3_prob','TIME_2','Q'),'TIME_2',ordinary(none),['TIME_2'],[],[equal(rodinpos('C_m3_prob',grd1,'\''),identifier(none,state),integer(none,2)),equal(rodinpos('C_m3_prob',grd2,'('),identifier(none,'TT'),boolean_true(none))],[],[assign(rodinpos('C_m3_prob',act1,')'),[identifier(none,new_now)],[add(none,identifier(none,new_now),identifier(none,b2))]),assign(rodinpos('C_m3_prob',act2,'*'),[identifier(none,'TT')],[boolean_false(none)])],[]),event(rodinpos('C_m3_prob','TIME_3','R'),'TIME_3',ordinary(none),['TIME_3'],[],[equal(rodinpos('C_m3_prob',grd1,'\''),identifier(none,state),integer(none,0)),equal(rodinpos('C_m3_prob',grd2,'('),identifier(none,'TT'),boolean_true(none))],[],[assign(rodinpos('C_m3_prob',act1,')'),[identifier(none,new_now)],[add(none,identifier(none,new_now),identifier(none,a))]),assign(rodinpos('C_m3_prob',act2,'*'),[identifier(none,'TT')],[boolean_false(none)])],[])])]),event_b_model(none,'C_m3',[sees(none,['C_c0','C_c1']),refines(none,'C_m2'),variables(none,[identifier(none,state),identifier(none,'TT'),identifier(none,t2_c),identifier(none,temp),identifier(none,new_now),identifier(none,t1_c)]),invariant(none,[member(rodinpos('C_m3',inv1,'I'),identifier(none,'TT'),bool_set(none)),member(rodinpos('C_m3',inv2,'K'),identifier(none,new_now),natural_set(none)),implication(rodinpos('C_m3',inv3,'O'),equal(none,identifier(none,'TT'),boolean_false(none)),equal(none,identifier(none,new_now),identifier(none,now))),implication(rodinpos('C_m3',inv4,'P'),conjunct(none,[equal(none,identifier(none,state),integer(none,1)),equal(none,identifier(none,'TT'),boolean_true(none))]),equal(none,add(none,identifier(none,new_now),identifier(none,b1)),identifier(none,now))),implication(rodinpos('C_m3',inv5,'Q'),conjunct(none,[equal(none,identifier(none,state),integer(none,2)),equal(none,identifier(none,'TT'),boolean_true(none))]),equal(none,add(none,identifier(none,new_now),identifier(none,b2)),identifier(none,now))),implication(rodinpos('C_m3',inv6,'R'),conjunct(none,[equal(none,identifier(none,state),integer(none,0)),equal(none,identifier(none,'TT'),boolean_true(none))]),equal(none,add(none,identifier(none,new_now),identifier(none,a)),identifier(none,now)))]),theorems(none,[implication(rodinpos('C_m3',inv7,'S'),conjunct(none,[equal(none,identifier(none,state),integer(none,0)),equal(none,identifier(none,'TT'),boolean_true(none))]),equal(none,min(none,event_b_comprehension_set(none,[identifier(none,t)],identifier(none,t),conjunct(none,[member(none,identifier(none,t),integer_set(none)),conjunct(none,[greater_equal(none,identifier(none,t),identifier(none,new_now)),equal(none,function(none,identifier(none,temp),[identifier(none,t)]),identifier(none,tM))])]))),add(none,identifier(none,new_now),identifier(none,a)))),implication(rodinpos('C_m3',inv8,'T'),conjunct(none,[equal(none,identifier(none,state),integer(none,1)),equal(none,identifier(none,'TT'),boolean_true(none))]),equal(none,min(none,event_b_comprehension_set(none,[identifier(none,t)],identifier(none,t),conjunct(none,[member(none,identifier(none,t),integer_set(none)),conjunct(none,[greater_equal(none,identifier(none,t),identifier(none,new_now)),equal(none,function(none,identifier(none,temp),[identifier(none,t)]),identifier(none,tm))])]))),add(none,identifier(none,new_now),identifier(none,b1)))),implication(rodinpos('C_m3',inv9,'U'),conjunct(none,[equal(none,identifier(none,state),integer(none,2)),equal(none,identifier(none,'TT'),boolean_true(none))]),equal(none,min(none,event_b_comprehension_set(none,[identifier(none,t)],identifier(none,t),conjunct(none,[member(none,identifier(none,t),integer_set(none)),conjunct(none,[greater_equal(none,identifier(none,t),identifier(none,new_now)),equal(none,function(none,identifier(none,temp),[identifier(none,t)]),identifier(none,tm))])]))),add(none,identifier(none,new_now),identifier(none,b2))))]),events(none,[event(rodinpos('C_m3','INITIALISATION','\''),'INITIALISATION',ordinary(none),['INITIALISATION'],[],[],[],[assign(rodinpos('C_m3',act1,internal1),[identifier(none,t1_c)],[event_b_comprehension_set(none,[identifier(none,t)],couple(none,[identifier(none,t),add(none,multiplication(none,integer(none,2),identifier(none,a)),identifier(none,b2))]),conjunct(none,[member(none,identifier(none,t),integer_set(none)),member(none,identifier(none,t),natural_set(none))]))]),assign(rodinpos('C_m3',act2,internal2),[identifier(none,t2_c)],[event_b_comprehension_set(none,[identifier(none,t)],couple(none,[identifier(none,t),identifier(none,a)]),conjunct(none,[member(none,identifier(none,t),integer_set(none)),member(none,identifier(none,t),natural_set(none))]))]),assign(rodinpos('C_m3',act3,')'),[identifier(none,state)],[integer(none,0)]),assign(rodinpos('C_m3',act7,internal4),[identifier(none,temp)],[event_b_comprehension_set(none,[identifier(none,t)],couple(none,[identifier(none,t),identifier(none,tM)]),conjunct(none,[member(none,identifier(none,t),integer_set(none)),member(none,identifier(none,t),natural_set(none))]))]),assign(rodinpos('C_m3',act8,'\''),[identifier(none,'TT')],[boolean_false(none)]),assign(rodinpos('C_m3',act9,'('),[identifier(none,new_now)],[integer(none,0)])],[]),event(rodinpos('C_m3',cool_rod1,'.'),cool_rod1,ordinary(none),[cool_rod1],[],[equal(rodinpos('C_m3',grd1,'\''),identifier(none,state),integer(none,0)),greater_equal(rodinpos('C_m3',grd2,'('),function(none,identifier(none,t1_c),[identifier(none,new_now)]),identifier(none,'T')),equal(rodinpos('C_m3',grd5,'2'),identifier(none,'TT'),boolean_false(none))],[equal(rodinpos('C_m3',grd3,'/'),function(none,identifier(none,temp),[identifier(none,new_now)]),identifier(none,tM)),member(rodinpos('C_m3',grd4,'1'),identifier(none,b1),natural_set(none))],[assign(rodinpos('C_m3',act1,')'),[identifier(none,state)],[integer(none,1)]),assign(rodinpos('C_m3',act3,'+'),[identifier(none,t2_c)],[overwrite(none,identifier(none,t2_c),event_b_comprehension_set(none,[identifier(none,t)],couple(none,[identifier(none,t),add(none,function(none,identifier(none,t2_c),[identifier(none,new_now)]),minus(none,identifier(none,t),identifier(none,new_now)))]),conjunct(none,[member(none,identifier(none,t),integer_set(none)),greater_equal(none,identifier(none,t),identifier(none,new_now))])))]),assign(rodinpos('C_m3',act4,'3'),[identifier(none,'TT')],[boolean_true(none)]),assign(rodinpos('C_m3',act5,'.'),[identifier(none,t1_c)],[overwrite(none,identifier(none,t1_c),event_b_comprehension_set(none,[identifier(none,t)],couple(none,[identifier(none,t),function(none,identifier(none,t1_c),[identifier(none,new_now)])]),conjunct(none,[member(none,identifier(none,t),integer_set(none)),greater_equal(none,identifier(none,t),identifier(none,new_now))])))]),assign(rodinpos('C_m3',act6,'0'),[identifier(none,temp)],[overwrite(none,identifier(none,temp),event_b_comprehension_set(none,[identifier(none,t)],couple(none,[identifier(none,t),minus(none,identifier(none,tM),multiplication(none,identifier(none,v1),minus(none,identifier(none,t),identifier(none,new_now))))]),conjunct(none,[member(none,identifier(none,t),integer_set(none)),greater_equal(none,identifier(none,t),identifier(none,new_now))])))])],[]),event(rodinpos('C_m3',cool_rod2,'/'),cool_rod2,ordinary(none),[cool_rod2],[],[equal(rodinpos('C_m3',grd1,'\''),identifier(none,state),integer(none,0)),greater_equal(rodinpos('C_m3',grd2,'('),function(none,identifier(none,t2_c),[identifier(none,new_now)]),identifier(none,'T')),equal(rodinpos('C_m3',grd5,'2'),identifier(none,'TT'),boolean_false(none))],[equal(rodinpos('C_m3',grd3,'/'),function(none,identifier(none,temp),[identifier(none,new_now)]),identifier(none,tM)),member(rodinpos('C_m3',grd4,'1'),identifier(none,b2),natural_set(none))],[assign(rodinpos('C_m3',act1,')'),[identifier(none,state)],[integer(none,2)]),assign(rodinpos('C_m3',act3,'+'),[identifier(none,t1_c)],[overwrite(none,identifier(none,t1_c),event_b_comprehension_set(none,[identifier(none,t)],couple(none,[identifier(none,t),add(none,function(none,identifier(none,t1_c),[identifier(none,new_now)]),minus(none,identifier(none,t),identifier(none,new_now)))]),conjunct(none,[member(none,identifier(none,t),integer_set(none)),greater_equal(none,identifier(none,t),identifier(none,new_now))])))]),assign(rodinpos('C_m3',act4,'-'),[identifier(none,'TT')],[boolean_true(none)]),assign(rodinpos('C_m3',act5,'.'),[identifier(none,t2_c)],[overwrite(none,identifier(none,t2_c),event_b_comprehension_set(none,[identifier(none,t)],couple(none,[identifier(none,t),function(none,identifier(none,t2_c),[identifier(none,new_now)])]),conjunct(none,[member(none,identifier(none,t),integer_set(none)),greater_equal(none,identifier(none,t),identifier(none,new_now))])))]),assign(rodinpos('C_m3',act6,'0'),[identifier(none,temp)],[overwrite(none,identifier(none,temp),event_b_comprehension_set(none,[identifier(none,t)],couple(none,[identifier(none,t),minus(none,identifier(none,tM),multiplication(none,identifier(none,v2),minus(none,identifier(none,t),identifier(none,new_now))))]),conjunct(none,[member(none,identifier(none,t),integer_set(none)),greater_equal(none,identifier(none,t),identifier(none,new_now))])))])],[]),event(rodinpos('C_m3',release_rod1,'0'),release_rod1,ordinary(none),[release_rod1],[],[equal(rodinpos('C_m3',grd1,'\''),identifier(none,state),integer(none,1)),equal(rodinpos('C_m3',grd4,'0'),identifier(none,'TT'),boolean_false(none))],[equal(rodinpos('C_m3',grd2,'-'),function(none,identifier(none,temp),[identifier(none,new_now)]),identifier(none,tm)),member(rodinpos('C_m3',grd3,'/'),identifier(none,a),natural_set(none))],[assign(rodinpos('C_m3',act1,'('),[identifier(none,state)],[integer(none,0)]),assign(rodinpos('C_m3',act2,')'),[identifier(none,t1_c)],[overwrite(none,identifier(none,t1_c),event_b_comprehension_set(none,[identifier(none,t)],couple(none,[identifier(none,t),minus(none,identifier(none,t),identifier(none,new_now))]),conjunct(none,[member(none,identifier(none,t),integer_set(none)),greater_equal(none,identifier(none,t),identifier(none,new_now))])))]),assign(rodinpos('C_m3',act3,'*'),[identifier(none,t2_c)],[overwrite(none,identifier(none,t2_c),event_b_comprehension_set(none,[identifier(none,t)],couple(none,[identifier(none,t),add(none,function(none,identifier(none,t2_c),[identifier(none,new_now)]),minus(none,identifier(none,t),identifier(none,new_now)))]),conjunct(none,[member(none,identifier(none,t),integer_set(none)),greater_equal(none,identifier(none,t),identifier(none,new_now))])))]),assign(rodinpos('C_m3',act4,','),[identifier(none,'TT')],[boolean_true(none)]),assign(rodinpos('C_m3',act5,'.'),[identifier(none,temp)],[overwrite(none,identifier(none,temp),event_b_comprehension_set(none,[identifier(none,t)],couple(none,[identifier(none,t),add(none,identifier(none,tm),multiplication(none,identifier(none,vr),minus(none,identifier(none,t),identifier(none,new_now))))]),conjunct(none,[member(none,identifier(none,t),integer_set(none)),greater_equal(none,identifier(none,t),identifier(none,new_now))])))])],[]),event(rodinpos('C_m3',release_rod2,'1'),release_rod2,ordinary(none),[release_rod2],[],[equal(rodinpos('C_m3',grd1,'\''),identifier(none,state),integer(none,2)),equal(rodinpos('C_m3',grd4,'/'),identifier(none,'TT'),boolean_false(none))],[equal(rodinpos('C_m3',grd2,','),function(none,identifier(none,temp),[identifier(none,new_now)]),identifier(none,tm)),member(rodinpos('C_m3',grd3,'.'),identifier(none,a),natural_set(none))],[assign(rodinpos('C_m3',act1,'('),[identifier(none,state)],[integer(none,0)]),assign(rodinpos('C_m3',act2,')'),[identifier(none,t1_c)],[overwrite(none,identifier(none,t1_c),event_b_comprehension_set(none,[identifier(none,t)],couple(none,[identifier(none,t),add(none,function(none,identifier(none,t1_c),[identifier(none,new_now)]),minus(none,identifier(none,t),identifier(none,new_now)))]),conjunct(none,[member(none,identifier(none,t),integer_set(none)),greater_equal(none,identifier(none,t),identifier(none,new_now))])))]),assign(rodinpos('C_m3',act3,'*'),[identifier(none,t2_c)],[overwrite(none,identifier(none,t2_c),event_b_comprehension_set(none,[identifier(none,t)],couple(none,[identifier(none,t),minus(none,identifier(none,t),identifier(none,new_now))]),conjunct(none,[member(none,identifier(none,t),integer_set(none)),greater_equal(none,identifier(none,t),identifier(none,new_now))])))]),assign(rodinpos('C_m3',act4,'+'),[identifier(none,'TT')],[boolean_true(none)]),assign(rodinpos('C_m3',act5,'-'),[identifier(none,temp)],[overwrite(none,identifier(none,temp),event_b_comprehension_set(none,[identifier(none,t)],couple(none,[identifier(none,t),add(none,identifier(none,tm),multiplication(none,identifier(none,vr),minus(none,identifier(none,t),identifier(none,new_now))))]),conjunct(none,[member(none,identifier(none,t),integer_set(none)),greater_equal(none,identifier(none,t),identifier(none,new_now))])))])],[]),event(rodinpos('C_m3','TIME_1','L'),'TIME_1',ordinary(none),[],[],[equal(rodinpos('C_m3',grd1,'\''),identifier(none,state),integer(none,1)),equal(rodinpos('C_m3',grd2,'('),identifier(none,'TT'),boolean_true(none))],[],[assign(rodinpos('C_m3',act1,')'),[identifier(none,new_now)],[add(none,identifier(none,new_now),identifier(none,b1))]),assign(rodinpos('C_m3',act2,'*'),[identifier(none,'TT')],[boolean_false(none)])],[]),event(rodinpos('C_m3','TIME_2','M'),'TIME_2',ordinary(none),[],[],[equal(rodinpos('C_m3',grd1,'\''),identifier(none,state),integer(none,2)),equal(rodinpos('C_m3',grd2,'('),identifier(none,'TT'),boolean_true(none))],[],[assign(rodinpos('C_m3',act1,')'),[identifier(none,new_now)],[add(none,identifier(none,new_now),identifier(none,b2))]),assign(rodinpos('C_m3',act2,'*'),[identifier(none,'TT')],[boolean_false(none)])],[]),event(rodinpos('C_m3','TIME_3','N'),'TIME_3',ordinary(none),[],[],[equal(rodinpos('C_m3',grd1,'\''),identifier(none,state),integer(none,0)),equal(rodinpos('C_m3',grd2,'('),identifier(none,'TT'),boolean_true(none))],[],[assign(rodinpos('C_m3',act1,')'),[identifier(none,new_now)],[add(none,identifier(none,new_now),identifier(none,a))]),assign(rodinpos('C_m3',act2,'*'),[identifier(none,'TT')],[boolean_false(none)])],[])])]),event_b_model(none,'C_m2',[sees(none,['C_c0','C_c1']),refines(none,'C_m1'),variables(none,[identifier(none,state),identifier(none,t2_c),identifier(none,now),identifier(none,temp),identifier(none,t1_c)]),invariant(none,[member(rodinpos('C_m2',inv1,'H'),identifier(none,temp),total_function(none,natural_set(none),integer_set(none))),equal(rodinpos('C_m2',inv2,'I'),identifier(none,tp),function(none,identifier(none,temp),[identifier(none,now)])),implication(rodinpos('C_m2',inv3,'J'),conjunct(none,[greater_equal(none,identifier(none,now),identifier(none,a)),equal(none,identifier(none,state),integer(none,0))]),equal(none,min(none,event_b_comprehension_set(none,[identifier(none,t)],identifier(none,t),conjunct(none,[member(none,identifier(none,t),integer_set(none)),conjunct(none,[greater_equal(none,identifier(none,t),minus(none,identifier(none,now),identifier(none,a))),equal(none,function(none,identifier(none,temp),[identifier(none,t)]),identifier(none,tM))])]))),identifier(none,now))),implication(rodinpos('C_m2',inv4,'K'),conjunct(none,[greater_equal(none,identifier(none,now),identifier(none,b1)),equal(none,identifier(none,state),integer(none,1))]),equal(none,min(none,event_b_comprehension_set(none,[identifier(none,t)],identifier(none,t),conjunct(none,[member(none,identifier(none,t),integer_set(none)),conjunct(none,[greater_equal(none,identifier(none,t),minus(none,identifier(none,now),identifier(none,b1))),equal(none,function(none,identifier(none,temp),[identifier(none,t)]),identifier(none,tm))])]))),identifier(none,now))),implication(rodinpos('C_m2',inv5,'L'),conjunct(none,[greater_equal(none,identifier(none,now),identifier(none,b2)),equal(none,identifier(none,state),integer(none,2))]),equal(none,min(none,event_b_comprehension_set(none,[identifier(none,t)],identifier(none,t),conjunct(none,[member(none,identifier(none,t),integer_set(none)),conjunct(none,[greater_equal(none,identifier(none,t),minus(none,identifier(none,now),identifier(none,b2))),equal(none,function(none,identifier(none,temp),[identifier(none,t)]),identifier(none,tm))])]))),identifier(none,now)))]),theorems(none,[]),events(none,[event(rodinpos('C_m2','INITIALISATION','\''),'INITIALISATION',ordinary(none),['INITIALISATION'],[],[],[],[assign(rodinpos('C_m2',act1,internal1),[identifier(none,t1_c)],[event_b_comprehension_set(none,[identifier(none,t)],couple(none,[identifier(none,t),add(none,multiplication(none,integer(none,2),identifier(none,a)),identifier(none,b2))]),conjunct(none,[member(none,identifier(none,t),integer_set(none)),member(none,identifier(none,t),natural_set(none))]))]),assign(rodinpos('C_m2',act2,internal2),[identifier(none,t2_c)],[event_b_comprehension_set(none,[identifier(none,t)],couple(none,[identifier(none,t),identifier(none,a)]),conjunct(none,[member(none,identifier(none,t),integer_set(none)),member(none,identifier(none,t),natural_set(none))]))]),assign(rodinpos('C_m2',act3,')'),[identifier(none,state)],[integer(none,0)]),assign(rodinpos('C_m2',act5,'('),[identifier(none,now)],[integer(none,0)]),assign(rodinpos('C_m2',act7,'\''),[identifier(none,temp)],[event_b_comprehension_set(none,[identifier(none,t)],couple(none,[identifier(none,t),identifier(none,tM)]),conjunct(none,[member(none,identifier(none,t),integer_set(none)),member(none,identifier(none,t),natural_set(none))]))])],[]),event(rodinpos('C_m2',cool_rod1,'.'),cool_rod1,ordinary(none),[cool_rod1],[],[equal(rodinpos('C_m2',grd1,'\''),identifier(none,state),integer(none,0)),greater_equal(rodinpos('C_m2',grd2,'('),function(none,identifier(none,t1_c),[identifier(none,now)]),identifier(none,'T'))],[equal(rodinpos('C_m2',grd3,'/'),function(none,identifier(none,temp),[identifier(none,now)]),identifier(none,tM)),member(rodinpos('C_m2',grd4,'1'),identifier(none,b1),natural_set(none))],[assign(rodinpos('C_m2',act1,')'),[identifier(none,state)],[integer(none,1)]),assign(rodinpos('C_m2',act3,'+'),[identifier(none,t2_c)],[overwrite(none,identifier(none,t2_c),event_b_comprehension_set(none,[identifier(none,t)],couple(none,[identifier(none,t),add(none,function(none,identifier(none,t2_c),[identifier(none,now)]),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('C_m2',act4,'-'),[identifier(none,now)],[add(none,identifier(none,now),identifier(none,b1))]),assign(rodinpos('C_m2',act5,'.'),[identifier(none,t1_c)],[overwrite(none,identifier(none,t1_c),event_b_comprehension_set(none,[identifier(none,t)],couple(none,[identifier(none,t),function(none,identifier(none,t1_c),[identifier(none,now)])]),conjunct(none,[member(none,identifier(none,t),integer_set(none)),greater_equal(none,identifier(none,t),identifier(none,now))])))]),assign(rodinpos('C_m2',act6,'0'),[identifier(none,temp)],[overwrite(none,identifier(none,temp),event_b_comprehension_set(none,[identifier(none,t)],couple(none,[identifier(none,t),minus(none,identifier(none,tM),multiplication(none,identifier(none,v1),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))])))])],[]),event(rodinpos('C_m2',cool_rod2,'/'),cool_rod2,ordinary(none),[cool_rod2],[],[equal(rodinpos('C_m2',grd1,'\''),identifier(none,state),integer(none,0)),greater_equal(rodinpos('C_m2',grd2,'('),function(none,identifier(none,t2_c),[identifier(none,now)]),identifier(none,'T'))],[equal(rodinpos('C_m2',grd3,'/'),function(none,identifier(none,temp),[identifier(none,now)]),identifier(none,tM)),member(rodinpos('C_m2',grd4,'1'),identifier(none,b2),natural_set(none))],[assign(rodinpos('C_m2',act1,')'),[identifier(none,state)],[integer(none,2)]),assign(rodinpos('C_m2',act3,'+'),[identifier(none,t1_c)],[overwrite(none,identifier(none,t1_c),event_b_comprehension_set(none,[identifier(none,t)],couple(none,[identifier(none,t),add(none,function(none,identifier(none,t1_c),[identifier(none,now)]),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('C_m2',act4,'-'),[identifier(none,now)],[add(none,identifier(none,now),identifier(none,b2))]),assign(rodinpos('C_m2',act5,'.'),[identifier(none,t2_c)],[overwrite(none,identifier(none,t2_c),event_b_comprehension_set(none,[identifier(none,t)],couple(none,[identifier(none,t),function(none,identifier(none,t2_c),[identifier(none,now)])]),conjunct(none,[member(none,identifier(none,t),integer_set(none)),greater_equal(none,identifier(none,t),identifier(none,now))])))]),assign(rodinpos('C_m2',act6,'0'),[identifier(none,temp)],[overwrite(none,identifier(none,temp),event_b_comprehension_set(none,[identifier(none,t)],couple(none,[identifier(none,t),minus(none,identifier(none,tM),multiplication(none,identifier(none,v2),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))])))])],[]),event(rodinpos('C_m2',release_rod1,'0'),release_rod1,ordinary(none),[release_rod1],[],[equal(rodinpos('C_m2',grd1,'\''),identifier(none,state),integer(none,1))],[equal(rodinpos('C_m2',grd2,'-'),function(none,identifier(none,temp),[identifier(none,now)]),identifier(none,tm)),member(rodinpos('C_m2',grd3,'/'),identifier(none,a),natural_set(none))],[assign(rodinpos('C_m2',act1,'('),[identifier(none,state)],[integer(none,0)]),assign(rodinpos('C_m2',act2,')'),[identifier(none,t1_c)],[overwrite(none,identifier(none,t1_c),event_b_comprehension_set(none,[identifier(none,t)],couple(none,[identifier(none,t),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('C_m2',act3,'*'),[identifier(none,t2_c)],[overwrite(none,identifier(none,t2_c),event_b_comprehension_set(none,[identifier(none,t)],couple(none,[identifier(none,t),add(none,function(none,identifier(none,t2_c),[identifier(none,now)]),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('C_m2',act4,','),[identifier(none,now)],[add(none,identifier(none,now),identifier(none,a))]),assign(rodinpos('C_m2',act5,'.'),[identifier(none,temp)],[overwrite(none,identifier(none,temp),event_b_comprehension_set(none,[identifier(none,t)],couple(none,[identifier(none,t),add(none,identifier(none,tm),multiplication(none,identifier(none,vr),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))])))])],[]),event(rodinpos('C_m2',release_rod2,'1'),release_rod2,ordinary(none),[release_rod2],[],[equal(rodinpos('C_m2',grd1,'\''),identifier(none,state),integer(none,2))],[equal(rodinpos('C_m2',grd2,','),function(none,identifier(none,temp),[identifier(none,now)]),identifier(none,tm)),member(rodinpos('C_m2',grd3,'.'),identifier(none,a),natural_set(none))],[assign(rodinpos('C_m2',act1,'('),[identifier(none,state)],[integer(none,0)]),assign(rodinpos('C_m2',act2,')'),[identifier(none,t1_c)],[overwrite(none,identifier(none,t1_c),event_b_comprehension_set(none,[identifier(none,t)],couple(none,[identifier(none,t),add(none,function(none,identifier(none,t1_c),[identifier(none,now)]),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('C_m2',act3,'*'),[identifier(none,t2_c)],[overwrite(none,identifier(none,t2_c),event_b_comprehension_set(none,[identifier(none,t)],couple(none,[identifier(none,t),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('C_m2',act4,'+'),[identifier(none,now)],[add(none,identifier(none,now),identifier(none,a))]),assign(rodinpos('C_m2',act5,'-'),[identifier(none,temp)],[overwrite(none,identifier(none,temp),event_b_comprehension_set(none,[identifier(none,t)],couple(none,[identifier(none,t),add(none,identifier(none,tm),multiplication(none,identifier(none,vr),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))])))])],[])])]),event_b_model(none,'C_m1',[sees(none,['C_c0','C_c1']),refines(none,'C_m0'),variables(none,[identifier(none,state),identifier(none,t2_c),identifier(none,now),identifier(none,tp),identifier(none,t1_c)]),invariant(none,[member(rodinpos('C_m1',inv1,':'),identifier(none,now),natural_set(none)),description(rodinpos('C_m1',inv3,';'),description_text(none,''),member(none,identifier(none,t1_c),total_function(none,natural_set(none),integer_set(none)))),description(rodinpos('C_m1',inv7,'C'),description_text(none,''),member(none,identifier(none,t2_c),total_function(none,natural_set(none),integer_set(none)))),description(rodinpos('C_m1',inv5,'>'),description_text(none,''),equal(none,identifier(none,t1),function(none,identifier(none,t1_c),[identifier(none,now)]))),description(rodinpos('C_m1',inv8,'D'),description_text(none,''),equal(none,identifier(none,t2),function(none,identifier(none,t2_c),[identifier(none,now)])))]),theorems(none,[implication(rodinpos('C_m1',thm,'E'),equal(none,identifier(none,state),integer(none,0)),disjunct(none,greater_equal(none,function(none,identifier(none,t1_c),[identifier(none,now)]),identifier(none,'T')),greater_equal(none,function(none,identifier(none,t2_c),[identifier(none,now)]),identifier(none,'T'))))]),events(none,[event(rodinpos('C_m1','INITIALISATION','\''),'INITIALISATION',ordinary(none),['INITIALISATION'],[],[],[],[assign(rodinpos('C_m1',act1,internal1),[identifier(none,t1_c)],[event_b_comprehension_set(none,[identifier(none,t)],couple(none,[identifier(none,t),add(none,multiplication(none,integer(none,2),identifier(none,a)),identifier(none,b2))]),conjunct(none,[member(none,identifier(none,t),integer_set(none)),member(none,identifier(none,t),natural_set(none))]))]),assign(rodinpos('C_m1',act2,internal2),[identifier(none,t2_c)],[event_b_comprehension_set(none,[identifier(none,t)],couple(none,[identifier(none,t),identifier(none,a)]),conjunct(none,[member(none,identifier(none,t),integer_set(none)),member(none,identifier(none,t),natural_set(none))]))]),assign(rodinpos('C_m1',act3,')'),[identifier(none,state)],[integer(none,0)]),assign(rodinpos('C_m1',act5,'('),[identifier(none,now)],[integer(none,0)]),assign(rodinpos('C_m1',act6,internal3),[identifier(none,tp)],[identifier(none,tM)])],[]),event(rodinpos('C_m1',cool_rod1,'.'),cool_rod1,ordinary(none),[cool_rod1],[],[equal(rodinpos('C_m1',grd1,'\''),identifier(none,state),integer(none,0)),greater_equal(rodinpos('C_m1',grd2,'('),function(none,identifier(none,t1_c),[identifier(none,now)]),identifier(none,'T'))],[equal(rodinpos('C_m1',grd3,'/'),identifier(none,tp),identifier(none,tM)),member(rodinpos('C_m1',grd4,'1'),identifier(none,b1),natural_set(none))],[assign(rodinpos('C_m1',act1,')'),[identifier(none,state)],[integer(none,1)]),assign(rodinpos('C_m1',act3,'+'),[identifier(none,t2_c)],[overwrite(none,identifier(none,t2_c),event_b_comprehension_set(none,[identifier(none,t)],couple(none,[identifier(none,t),add(none,function(none,identifier(none,t2_c),[identifier(none,now)]),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('C_m1',act4,'-'),[identifier(none,now)],[add(none,identifier(none,now),identifier(none,b1))]),assign(rodinpos('C_m1',act5,'.'),[identifier(none,t1_c)],[overwrite(none,identifier(none,t1_c),event_b_comprehension_set(none,[identifier(none,t)],couple(none,[identifier(none,t),function(none,identifier(none,t1_c),[identifier(none,now)])]),conjunct(none,[member(none,identifier(none,t),integer_set(none)),greater_equal(none,identifier(none,t),identifier(none,now))])))]),assign(rodinpos('C_m1',act6,'0'),[identifier(none,tp)],[identifier(none,tm)])],[]),event(rodinpos('C_m1',cool_rod2,'/'),cool_rod2,ordinary(none),[cool_rod2],[],[equal(rodinpos('C_m1',grd1,'\''),identifier(none,state),integer(none,0)),greater_equal(rodinpos('C_m1',grd2,'('),function(none,identifier(none,t2_c),[identifier(none,now)]),identifier(none,'T'))],[equal(rodinpos('C_m1',grd3,'/'),identifier(none,tp),identifier(none,tM)),member(rodinpos('C_m1',grd4,'1'),identifier(none,b2),natural_set(none))],[assign(rodinpos('C_m1',act1,')'),[identifier(none,state)],[integer(none,2)]),assign(rodinpos('C_m1',act3,'+'),[identifier(none,t1_c)],[overwrite(none,identifier(none,t1_c),event_b_comprehension_set(none,[identifier(none,t)],couple(none,[identifier(none,t),add(none,function(none,identifier(none,t1_c),[identifier(none,now)]),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('C_m1',act4,'-'),[identifier(none,now)],[add(none,identifier(none,now),identifier(none,b2))]),assign(rodinpos('C_m1',act5,'.'),[identifier(none,t2_c)],[overwrite(none,identifier(none,t2_c),event_b_comprehension_set(none,[identifier(none,t)],couple(none,[identifier(none,t),function(none,identifier(none,t2_c),[identifier(none,now)])]),conjunct(none,[member(none,identifier(none,t),integer_set(none)),greater_equal(none,identifier(none,t),identifier(none,now))])))]),assign(rodinpos('C_m1',act6,'0'),[identifier(none,tp)],[identifier(none,tm)])],[]),event(rodinpos('C_m1',release_rod1,'0'),release_rod1,ordinary(none),[release_rod1],[],[equal(rodinpos('C_m1',grd1,'\''),identifier(none,state),integer(none,1))],[equal(rodinpos('C_m1',grd2,'-'),identifier(none,tp),identifier(none,tm)),member(rodinpos('C_m1',grd3,'/'),identifier(none,a),natural_set(none))],[assign(rodinpos('C_m1',act1,'('),[identifier(none,state)],[integer(none,0)]),assign(rodinpos('C_m1',act2,')'),[identifier(none,t1_c)],[overwrite(none,identifier(none,t1_c),event_b_comprehension_set(none,[identifier(none,t)],couple(none,[identifier(none,t),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('C_m1',act3,'*'),[identifier(none,t2_c)],[overwrite(none,identifier(none,t2_c),event_b_comprehension_set(none,[identifier(none,t)],couple(none,[identifier(none,t),add(none,function(none,identifier(none,t2_c),[identifier(none,now)]),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('C_m1',act4,','),[identifier(none,now)],[add(none,identifier(none,now),identifier(none,a))]),assign(rodinpos('C_m1',act5,'.'),[identifier(none,tp)],[identifier(none,tM)])],[]),event(rodinpos('C_m1',release_rod2,'1'),release_rod2,ordinary(none),[release_rod2],[],[equal(rodinpos('C_m1',grd1,'\''),identifier(none,state),integer(none,2))],[equal(rodinpos('C_m1',grd2,','),identifier(none,tp),identifier(none,tm)),member(rodinpos('C_m1',grd3,'.'),identifier(none,a),natural_set(none))],[assign(rodinpos('C_m1',act1,'('),[identifier(none,state)],[integer(none,0)]),assign(rodinpos('C_m1',act2,')'),[identifier(none,t1_c)],[overwrite(none,identifier(none,t1_c),event_b_comprehension_set(none,[identifier(none,t)],couple(none,[identifier(none,t),add(none,function(none,identifier(none,t1_c),[identifier(none,now)]),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('C_m1',act3,'*'),[identifier(none,t2_c)],[overwrite(none,identifier(none,t2_c),event_b_comprehension_set(none,[identifier(none,t)],couple(none,[identifier(none,t),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('C_m1',act4,'+'),[identifier(none,now)],[add(none,identifier(none,now),identifier(none,a))]),assign(rodinpos('C_m1',act5,'-'),[identifier(none,tp)],[identifier(none,tM)])],[])])]),event_b_model(none,'C_m0',[sees(none,['C_c0']),variables(none,[identifier(none,state),identifier(none,t1),identifier(none,t2),identifier(none,tp)]),invariant(none,[member(rodinpos('C_m0',inv1,')'),identifier(none,t1),natural_set(none)),member(rodinpos('C_m0',inv2,'+'),identifier(none,t2),natural_set(none)),member(rodinpos('C_m0',inv3,'-'),identifier(none,state),set_extension(none,[integer(none,0),integer(none,1),integer(none,2)])),implication(rodinpos('C_m0',inv4,'2'),conjunct(none,[equal(none,identifier(none,state),integer(none,0)),greater_equal(none,identifier(none,t1),identifier(none,'T'))]),greater_equal(none,identifier(none,t2),identifier(none,a))),implication(rodinpos('C_m0',inv5,'3'),conjunct(none,[equal(none,identifier(none,state),integer(none,0)),greater_equal(none,identifier(none,t2),identifier(none,'T'))]),greater_equal(none,identifier(none,t1),identifier(none,a))),implication(rodinpos('C_m0',inv6,'4'),equal(none,identifier(none,state),integer(none,1)),greater_equal(none,identifier(none,t2),add(none,identifier(none,a),identifier(none,b1)))),implication(rodinpos('C_m0',inv7,'5'),equal(none,identifier(none,state),integer(none,2)),greater_equal(none,identifier(none,t1),add(none,identifier(none,a),identifier(none,b2)))),implication(rodinpos('C_m0',inv8,'7'),conjunct(none,[equal(none,identifier(none,state),integer(none,0)),greater_equal(none,identifier(none,t1),identifier(none,'T'))]),conjunct(none,[greater_equal(none,identifier(none,t1),add(none,multiplication(none,integer(none,2),identifier(none,a)),identifier(none,b2))),equal(none,identifier(none,t2),identifier(none,a))])),implication(rodinpos('C_m0',inv9,'8'),conjunct(none,[equal(none,identifier(none,state),integer(none,0)),greater_equal(none,identifier(none,t2),identifier(none,'T'))]),conjunct(none,[greater_equal(none,identifier(none,t2),add(none,multiplication(none,integer(none,2),identifier(none,a)),identifier(none,b1))),equal(none,identifier(none,t1),identifier(none,a))])),implication(rodinpos('C_m0',inv10,'9'),equal(none,identifier(none,state),integer(none,0)),disjunct(none,greater_equal(none,identifier(none,t1),identifier(none,'T')),greater_equal(none,identifier(none,t2),identifier(none,'T')))),member(rodinpos('C_m0',inv11,';'),identifier(none,tp),natural_set(none)),implication(rodinpos('C_m0',inv12,'='),equal(none,identifier(none,state),integer(none,1)),equal(none,identifier(none,tp),identifier(none,tm))),implication(rodinpos('C_m0',inv13,'>'),equal(none,identifier(none,state),integer(none,2)),equal(none,identifier(none,tp),identifier(none,tm))),implication(rodinpos('C_m0',inv14,'?'),equal(none,identifier(none,state),integer(none,0)),equal(none,identifier(none,tp),identifier(none,tM)))]),theorems(none,[]),events(none,[event(rodinpos('C_m0','INITIALISATION','\''),'INITIALISATION',ordinary(none),[],[],[],[],[assign(rodinpos('C_m0',act1,'\''),[identifier(none,t1)],[add(none,multiplication(none,integer(none,2),identifier(none,a)),identifier(none,b2))]),assign(rodinpos('C_m0',act2,'('),[identifier(none,t2)],[identifier(none,a)]),assign(rodinpos('C_m0',act3,')'),[identifier(none,state)],[integer(none,0)]),assign(rodinpos('C_m0',act4,'*'),[identifier(none,tp)],[identifier(none,tM)])],[]),event(rodinpos('C_m0',cool_rod1,'.'),cool_rod1,ordinary(none),[],[],[equal(rodinpos('C_m0',grd1,'\''),identifier(none,state),integer(none,0)),greater_equal(rodinpos('C_m0',grd2,'('),identifier(none,t1),identifier(none,'T'))],[equal(rodinpos('C_m0',grd3,','),identifier(none,tp),identifier(none,tM))],[assign(rodinpos('C_m0',act1,')'),[identifier(none,state)],[integer(none,1)]),assign(rodinpos('C_m0',act3,'+'),[identifier(none,t2)],[add(none,identifier(none,t2),identifier(none,b1))]),assign(rodinpos('C_m0',act4,'-'),[identifier(none,tp)],[identifier(none,tm)])],[]),event(rodinpos('C_m0',cool_rod2,'/'),cool_rod2,ordinary(none),[],[],[equal(rodinpos('C_m0',grd1,'\''),identifier(none,state),integer(none,0)),greater_equal(rodinpos('C_m0',grd2,'('),identifier(none,t2),identifier(none,'T'))],[equal(rodinpos('C_m0',grd3,','),identifier(none,tp),identifier(none,tM))],[assign(rodinpos('C_m0',act1,')'),[identifier(none,state)],[integer(none,2)]),assign(rodinpos('C_m0',act3,'+'),[identifier(none,t1)],[add(none,identifier(none,t1),identifier(none,b2))]),assign(rodinpos('C_m0',act4,'-'),[identifier(none,tp)],[identifier(none,tm)])],[]),event(rodinpos('C_m0',release_rod1,'0'),release_rod1,ordinary(none),[],[],[equal(rodinpos('C_m0',grd1,'\''),identifier(none,state),integer(none,1))],[equal(rodinpos('C_m0',grd2,'+'),identifier(none,tp),identifier(none,tm))],[assign(rodinpos('C_m0',act1,'('),[identifier(none,state)],[integer(none,0)]),assign(rodinpos('C_m0',act2,')'),[identifier(none,t1)],[identifier(none,a)]),assign(rodinpos('C_m0',act3,'*'),[identifier(none,t2)],[add(none,identifier(none,t2),identifier(none,a))]),assign(rodinpos('C_m0',act4,','),[identifier(none,tp)],[identifier(none,tM)])],[]),event(rodinpos('C_m0',release_rod2,'1'),release_rod2,ordinary(none),[],[],[equal(rodinpos('C_m0',grd1,'\''),identifier(none,state),integer(none,2))],[equal(rodinpos('C_m0',grd2,'+'),identifier(none,tp),identifier(none,tm))],[assign(rodinpos('C_m0',act1,'('),[identifier(none,state)],[integer(none,0)]),assign(rodinpos('C_m0',act2,')'),[identifier(none,t1)],[add(none,identifier(none,t1),identifier(none,a))]),assign(rodinpos('C_m0',act3,'*'),[identifier(none,t2)],[identifier(none,a)]),assign(rodinpos('C_m0',act4,','),[identifier(none,tp)],[identifier(none,tM)])],[])])])],[event_b_context(none,'C_c0',[extends(none,[]),constants(none,[identifier(none,'T'),identifier(none,a),identifier(none,b1),identifier(none,b2),identifier(none,tM),identifier(none,tm),identifier(none,v1),identifier(none,v2),identifier(none,vr)]),abstract_constants(none,[]),axioms(none,[member(rodinpos('C_c0',axm1,'('),identifier(none,a),natural_set(none)),member(rodinpos('C_c0',axm2,'*'),identifier(none,b1),natural_set(none)),member(rodinpos('C_c0',axm3,','),identifier(none,b2),natural_set(none)),member(rodinpos('C_c0',axm4,'.'),identifier(none,'T'),natural_set(none)),greater_equal(rodinpos('C_c0',axm5,'/'),add(none,multiplication(none,integer(none,2),identifier(none,a)),identifier(none,b1)),identifier(none,'T')),greater_equal(rodinpos('C_c0',axm6,'0'),add(none,multiplication(none,integer(none,2),identifier(none,a)),identifier(none,b2)),identifier(none,'T')),less(rodinpos('C_c0',axm7,'1'),identifier(none,a),identifier(none,'T')),member(rodinpos('C_c0',axm8,'3'),identifier(none,tm),natural_set(none)),member(rodinpos('C_c0',axm9,'5'),identifier(none,tM),natural_set(none)),greater(rodinpos('C_c0',axm10,'6'),identifier(none,tM),identifier(none,tm)),member(rodinpos('C_c0',axm11,'8'),identifier(none,v1),natural_set(none)),member(rodinpos('C_c0',axm12,':'),identifier(none,v2),natural_set(none)),member(rodinpos('C_c0',axm13,'='),identifier(none,vr),natural_set(none)),equal(rodinpos('C_c0',axm14,'>'),multiplication(none,identifier(none,v1),identifier(none,b1)),minus(none,identifier(none,tM),identifier(none,tm))),equal(rodinpos('C_c0',axm15,'?'),multiplication(none,identifier(none,v2),identifier(none,b2)),minus(none,identifier(none,tM),identifier(none,tm))),equal(rodinpos('C_c0',axm16,'@'),multiplication(none,identifier(none,vr),identifier(none,a)),minus(none,identifier(none,tM),identifier(none,tm))),forall(rodinpos('C_c0','prob-ignore-axm17','_J7sYME4CEfG9muiHIIMeLw'),[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)),equal(none,multiplication(none,identifier(none,x),identifier(none,y)),multiplication(none,identifier(none,x),identifier(none,z)))])])]),equal(none,identifier(none,y),identifier(none,z))))]),theorems(none,[]),sets(none,[])]),event_b_context(none,'C_c1',[extends(none,['C_c0']),constants(none,[identifier(none,p),identifier(none,q),identifier(none,r)]),abstract_constants(none,[]),axioms(none,[greater(rodinpos('C_c1',axm1,')'),identifier(none,p),integer(none,0)),greater(rodinpos('C_c1',axm2,'+'),identifier(none,q),integer(none,0)),greater(rodinpos('C_c1',axm3,'-'),identifier(none,r),integer(none,0))]),theorems(none,[]),sets(none,[])]),event_b_context(none,'C_c0_prob',[extends(none,['C_c0']),constants(none,[]),abstract_constants(none,[]),axioms(none,[equal(rodinpos('C_c0_prob',prob1,'_lGOP0E4CEfG9muiHIIMeLw'),identifier(none,a),integer(none,8)),equal(rodinpos('C_c0_prob',prob2,'_lGO24E4CEfG9muiHIIMeLw'),identifier(none,b1),integer(none,2)),equal(rodinpos('C_c0_prob',prob3,'_lGO24U4CEfG9muiHIIMeLw'),identifier(none,b2),integer(none,2)),equal(rodinpos('C_c0_prob',prob4,'_lGO24k4CEfG9muiHIIMeLw'),identifier(none,'T'),integer(none,18)),conjunct(rodinpos('C_c0_prob',prob5,'_JXRAAE4DEfG9muiHIIMeLw'),[equal(none,identifier(none,tM),integer(none,10)),conjunct(none,[equal(none,identifier(none,tm),integer(none,2)),conjunct(none,[equal(none,identifier(none,v1),integer(none,4)),equal(none,identifier(none,v2),integer(none,4))])])])]),theorems(none,[]),sets(none,[])]),event_b_context(none,'C_c1_prob',[extends(none,['C_c1','C_c0_prob']),constants(none,[]),abstract_constants(none,[]),axioms(none,[]),theorems(none,[]),sets(none,[])])],[exporter_version(3),po('C_m3','Well-definedness of Theorem',[invariant(inv7)],true),po('C_m3','Theorem',[invariant(inv7)],true),po('C_m3','Well-definedness of Theorem',[invariant(inv8)],true),po('C_m3','Theorem',[invariant(inv8)],true),po('C_m3','Well-definedness of Theorem',[invariant(inv9)],true),po('C_m3','Theorem',[invariant(inv9)],true),po('C_m3','Invariant  establishment',[event('INITIALISATION'),event('INITIALISATION'),invariant(inv2)],true),po('C_m3','Invariant  establishment',[event('INITIALISATION'),event('INITIALISATION'),invariant(inv3)],true),po('C_m3','Invariant  establishment',[event('INITIALISATION'),event('INITIALISATION'),invariant(inv4)],true),po('C_m3','Invariant  establishment',[event('INITIALISATION'),event('INITIALISATION'),invariant(inv5)],true),po('C_m3','Invariant  establishment',[event('INITIALISATION'),event('INITIALISATION'),invariant(inv6)],true),po('C_m3','Action simulation',[event('INITIALISATION'),action(act7),event('INITIALISATION')],true),po('C_m3','Well-definedness of Guard',[guard(grd2),event(cool_rod1)],true),po('C_m3','Well-definedness of Theorem',[guard(grd3),event(cool_rod1)],true),po('C_m3','Theorem',[guard(grd3),event(cool_rod1)],true),po('C_m3','Theorem',[guard(grd4),event(cool_rod1)],true),po('C_m3','Invariant  preservation',[event(cool_rod1),event(cool_rod1),invariant(inv3)],true),po('C_m3','Invariant  preservation',[event(cool_rod1),event(cool_rod1),invariant(inv4)],true),po('C_m3','Invariant  preservation',[event(cool_rod1),event(cool_rod1),invariant(inv5)],true),po('C_m3','Invariant  preservation',[event(cool_rod1),event(cool_rod1),invariant(inv6)],true),po('C_m3','Guard strengthening (split)',[event(cool_rod1),guard(grd2),event(cool_rod1),event(cool_rod1)],true),po('C_m3','Well-definedness of action',[action(act3)],true),po('C_m3','Well-definedness of action',[action(act5)],true),po('C_m3','Action simulation',[event(cool_rod1),action(act3),event(cool_rod1)],true),po('C_m3','Action simulation',[event(cool_rod1),action(act5),event(cool_rod1)],true),po('C_m3','Action simulation',[event(cool_rod1),action(act6),event(cool_rod1)],true),po('C_m3','Well-definedness of Guard',[guard(grd2),event(cool_rod2)],true),po('C_m3','Well-definedness of Theorem',[guard(grd3),event(cool_rod2)],true),po('C_m3','Theorem',[guard(grd3),event(cool_rod2)],true),po('C_m3','Theorem',[guard(grd4),event(cool_rod2)],true),po('C_m3','Invariant  preservation',[event(cool_rod2),event(cool_rod2),invariant(inv3)],true),po('C_m3','Invariant  preservation',[event(cool_rod2),event(cool_rod2),invariant(inv4)],true),po('C_m3','Invariant  preservation',[event(cool_rod2),event(cool_rod2),invariant(inv5)],true),po('C_m3','Invariant  preservation',[event(cool_rod2),event(cool_rod2),invariant(inv6)],true),po('C_m3','Guard strengthening (split)',[event(cool_rod2),guard(grd2),event(cool_rod2),event(cool_rod2)],true),po('C_m3','Well-definedness of action',[action(act3)],true),po('C_m3','Well-definedness of action',[action(act5)],true),po('C_m3','Action simulation',[event(cool_rod2),action(act3),event(cool_rod2)],true),po('C_m3','Action simulation',[event(cool_rod2),action(act5),event(cool_rod2)],true),po('C_m3','Action simulation',[event(cool_rod2),action(act6),event(cool_rod2)],true),po('C_m3','Well-definedness of Theorem',[guard(grd2),event(release_rod1)],true),po('C_m3','Theorem',[guard(grd2),event(release_rod1)],true),po('C_m3','Theorem',[guard(grd3),event(release_rod1)],true),po('C_m3','Invariant  preservation',[event(release_rod1),event(release_rod1),invariant(inv3)],true),po('C_m3','Invariant  preservation',[event(release_rod1),event(release_rod1),invariant(inv4)],true),po('C_m3','Invariant  preservation',[event(release_rod1),event(release_rod1),invariant(inv5)],true),po('C_m3','Invariant  preservation',[event(release_rod1),event(release_rod1),invariant(inv6)],true),po('C_m3','Well-definedness of action',[action(act3)],true),po('C_m3','Action simulation',[event(release_rod1),action(act2),event(release_rod1)],true),po('C_m3','Action simulation',[event(release_rod1),action(act3),event(release_rod1)],true),po('C_m3','Action simulation',[event(release_rod1),action(act5),event(release_rod1)],true),po('C_m3','Well-definedness of Theorem',[guard(grd2),event(release_rod2)],true),po('C_m3','Theorem',[guard(grd2),event(release_rod2)],true),po('C_m3','Theorem',[guard(grd3),event(release_rod2)],true),po('C_m3','Invariant  preservation',[event(release_rod2),event(release_rod2),invariant(inv3)],true),po('C_m3','Invariant  preservation',[event(release_rod2),event(release_rod2),invariant(inv4)],true),po('C_m3','Invariant  preservation',[event(release_rod2),event(release_rod2),invariant(inv5)],true),po('C_m3','Invariant  preservation',[event(release_rod2),event(release_rod2),invariant(inv6)],true),po('C_m3','Well-definedness of action',[action(act2)],true),po('C_m3','Action simulation',[event(release_rod2),action(act2),event(release_rod2)],true),po('C_m3','Action simulation',[event(release_rod2),action(act3),event(release_rod2)],true),po('C_m3','Action simulation',[event(release_rod2),action(act5),event(release_rod2)],true),po('C_m3','Invariant  preservation',[event('TIME_1'),invariant(inv2)],true),po('C_m3','Invariant  preservation',[event('TIME_1'),invariant(inv3)],true),po('C_m3','Invariant  preservation',[event('TIME_1'),invariant(inv4)],true),po('C_m3','Invariant  preservation',[event('TIME_1'),invariant(inv5)],true),po('C_m3','Invariant  preservation',[event('TIME_1'),invariant(inv6)],true),po('C_m3','Invariant  preservation',[event('TIME_2'),invariant(inv2)],true),po('C_m3','Invariant  preservation',[event('TIME_2'),invariant(inv3)],true),po('C_m3','Invariant  preservation',[event('TIME_2'),invariant(inv4)],true),po('C_m3','Invariant  preservation',[event('TIME_2'),invariant(inv5)],true),po('C_m3','Invariant  preservation',[event('TIME_2'),invariant(inv6)],true),po('C_m3','Invariant  preservation',[event('TIME_3'),invariant(inv2)],true),po('C_m3','Invariant  preservation',[event('TIME_3'),invariant(inv3)],true),po('C_m3','Invariant  preservation',[event('TIME_3'),invariant(inv4)],true),po('C_m3','Invariant  preservation',[event('TIME_3'),invariant(inv5)],true),po('C_m3','Invariant  preservation',[event('TIME_3'),invariant(inv6)],true),po('C_m1','Well-definedness of Invariant',[invariant(inv5)],true),po('C_m1','Well-definedness of Invariant',[invariant(inv8)],true),po('C_m1','Well-definedness of Theorem',[invariant(thm)],true),po('C_m1','Theorem',[invariant(thm)],true),po('C_m1','Invariant  establishment',[event('INITIALISATION'),event('INITIALISATION'),invariant(inv1)],true),po('C_m1','Invariant  establishment',[event('INITIALISATION'),event('INITIALISATION'),invariant(inv3)],true),po('C_m1','Invariant  establishment',[event('INITIALISATION'),event('INITIALISATION'),invariant(inv7)],true),po('C_m1','Invariant  establishment',[event('INITIALISATION'),event('INITIALISATION'),invariant(inv5)],true),po('C_m1','Invariant  establishment',[event('INITIALISATION'),event('INITIALISATION'),invariant(inv8)],true),po('C_m1','Action simulation',[event('INITIALISATION'),action(act3),event('INITIALISATION')],true),po('C_m1','Action simulation',[event('INITIALISATION'),action(act4),event('INITIALISATION')],true),po('C_m1','Well-definedness of Guard',[guard(grd2),event(cool_rod1)],true),po('C_m1','Theorem',[guard(grd3),event(cool_rod1)],true),po('C_m1','Theorem',[guard(grd4),event(cool_rod1)],true),po('C_m1','Invariant  preservation',[event(cool_rod1),event(cool_rod1),invariant(inv1)],true),po('C_m1','Invariant  preservation',[event(cool_rod1),event(cool_rod1),invariant(inv3)],true),po('C_m1','Invariant  preservation',[event(cool_rod1),event(cool_rod1),invariant(inv7)],true),po('C_m1','Invariant  preservation',[event(cool_rod1),event(cool_rod1),invariant(inv5)],true),po('C_m1','Invariant  preservation',[event(cool_rod1),event(cool_rod1),invariant(inv8)],true),po('C_m1','Guard strengthening (split)',[event(cool_rod1),guard(grd2),event(cool_rod1),event(cool_rod1)],true),po('C_m1','Well-definedness of action',[action(act3)],true),po('C_m1','Well-definedness of action',[action(act5)],true),po('C_m1','Action simulation',[event(cool_rod1),action(act4),event(cool_rod1)],true),po('C_m1','Well-definedness of Guard',[guard(grd2),event(cool_rod2)],true),po('C_m1','Theorem',[guard(grd3),event(cool_rod2)],true),po('C_m1','Theorem',[guard(grd4),event(cool_rod2)],true),po('C_m1','Invariant  preservation',[event(cool_rod2),event(cool_rod2),invariant(inv1)],true),po('C_m1','Invariant  preservation',[event(cool_rod2),event(cool_rod2),invariant(inv3)],true),po('C_m1','Invariant  preservation',[event(cool_rod2),event(cool_rod2),invariant(inv7)],true),po('C_m1','Invariant  preservation',[event(cool_rod2),event(cool_rod2),invariant(inv5)],true),po('C_m1','Invariant  preservation',[event(cool_rod2),event(cool_rod2),invariant(inv8)],true),po('C_m1','Guard strengthening (split)',[event(cool_rod2),guard(grd2),event(cool_rod2),event(cool_rod2)],true),po('C_m1','Well-definedness of action',[action(act3)],true),po('C_m1','Well-definedness of action',[action(act5)],true),po('C_m1','Action simulation',[event(cool_rod2),action(act4),event(cool_rod2)],true),po('C_m1','Theorem',[guard(grd3),event(release_rod1)],true),po('C_m1','Invariant  preservation',[event(release_rod1),event(release_rod1),invariant(inv1)],true),po('C_m1','Invariant  preservation',[event(release_rod1),event(release_rod1),invariant(inv3)],true),po('C_m1','Invariant  preservation',[event(release_rod1),event(release_rod1),invariant(inv7)],true),po('C_m1','Invariant  preservation',[event(release_rod1),event(release_rod1),invariant(inv5)],true),po('C_m1','Invariant  preservation',[event(release_rod1),event(release_rod1),invariant(inv8)],true),po('C_m1','Well-definedness of action',[action(act3)],true),po('C_m1','Action simulation',[event(release_rod1),action(act4),event(release_rod1)],true),po('C_m1','Theorem',[guard(grd3),event(release_rod2)],true),po('C_m1','Invariant  preservation',[event(release_rod2),event(release_rod2),invariant(inv1)],true),po('C_m1','Invariant  preservation',[event(release_rod2),event(release_rod2),invariant(inv3)],true),po('C_m1','Invariant  preservation',[event(release_rod2),event(release_rod2),invariant(inv7)],true),po('C_m1','Invariant  preservation',[event(release_rod2),event(release_rod2),invariant(inv5)],true),po('C_m1','Invariant  preservation',[event(release_rod2),event(release_rod2),invariant(inv8)],true),po('C_m1','Well-definedness of action',[action(act2)],true),po('C_m1','Action simulation',[event(release_rod2),action(act4),event(release_rod2)],true),po('C_m0','Invariant  establishment',[event('INITIALISATION'),invariant(inv1)],true),po('C_m0','Invariant  establishment',[event('INITIALISATION'),invariant(inv2)],true),po('C_m0','Invariant  establishment',[event('INITIALISATION'),invariant(inv3)],true),po('C_m0','Invariant  establishment',[event('INITIALISATION'),invariant(inv4)],true),po('C_m0','Invariant  establishment',[event('INITIALISATION'),invariant(inv5)],true),po('C_m0','Invariant  establishment',[event('INITIALISATION'),invariant(inv6)],true),po('C_m0','Invariant  establishment',[event('INITIALISATION'),invariant(inv7)],true),po('C_m0','Invariant  establishment',[event('INITIALISATION'),invariant(inv8)],true),po('C_m0','Invariant  establishment',[event('INITIALISATION'),invariant(inv9)],true),po('C_m0','Invariant  establishment',[event('INITIALISATION'),invariant(inv10)],true),po('C_m0','Invariant  establishment',[event('INITIALISATION'),invariant(inv11)],true),po('C_m0','Invariant  establishment',[event('INITIALISATION'),invariant(inv12)],true),po('C_m0','Invariant  establishment',[event('INITIALISATION'),invariant(inv13)],true),po('C_m0','Invariant  establishment',[event('INITIALISATION'),invariant(inv14)],true),po('C_m0','Theorem',[guard(grd3),event(cool_rod1)],true),po('C_m0','Invariant  preservation',[event(cool_rod1),invariant(inv2)],true),po('C_m0','Invariant  preservation',[event(cool_rod1),invariant(inv3)],true),po('C_m0','Invariant  preservation',[event(cool_rod1),invariant(inv4)],true),po('C_m0','Invariant  preservation',[event(cool_rod1),invariant(inv5)],true),po('C_m0','Invariant  preservation',[event(cool_rod1),invariant(inv6)],true),po('C_m0','Invariant  preservation',[event(cool_rod1),invariant(inv7)],true),po('C_m0','Invariant  preservation',[event(cool_rod1),invariant(inv8)],true),po('C_m0','Invariant  preservation',[event(cool_rod1),invariant(inv9)],true),po('C_m0','Invariant  preservation',[event(cool_rod1),invariant(inv10)],true),po('C_m0','Invariant  preservation',[event(cool_rod1),invariant(inv11)],true),po('C_m0','Invariant  preservation',[event(cool_rod1),invariant(inv12)],true),po('C_m0','Invariant  preservation',[event(cool_rod1),invariant(inv13)],true),po('C_m0','Invariant  preservation',[event(cool_rod1),invariant(inv14)],true),po('C_m0','Theorem',[guard(grd3),event(cool_rod2)],true),po('C_m0','Invariant  preservation',[event(cool_rod2),invariant(inv1)],true),po('C_m0','Invariant  preservation',[event(cool_rod2),invariant(inv3)],true),po('C_m0','Invariant  preservation',[event(cool_rod2),invariant(inv4)],true),po('C_m0','Invariant  preservation',[event(cool_rod2),invariant(inv5)],true),po('C_m0','Invariant  preservation',[event(cool_rod2),invariant(inv6)],true),po('C_m0','Invariant  preservation',[event(cool_rod2),invariant(inv7)],true),po('C_m0','Invariant  preservation',[event(cool_rod2),invariant(inv8)],true),po('C_m0','Invariant  preservation',[event(cool_rod2),invariant(inv9)],true),po('C_m0','Invariant  preservation',[event(cool_rod2),invariant(inv10)],true),po('C_m0','Invariant  preservation',[event(cool_rod2),invariant(inv11)],true),po('C_m0','Invariant  preservation',[event(cool_rod2),invariant(inv12)],true),po('C_m0','Invariant  preservation',[event(cool_rod2),invariant(inv13)],true),po('C_m0','Invariant  preservation',[event(cool_rod2),invariant(inv14)],true),po('C_m0','Theorem',[guard(grd2),event(release_rod1)],true),po('C_m0','Invariant  preservation',[event(release_rod1),invariant(inv1)],true),po('C_m0','Invariant  preservation',[event(release_rod1),invariant(inv2)],true),po('C_m0','Invariant  preservation',[event(release_rod1),invariant(inv3)],true),po('C_m0','Invariant  preservation',[event(release_rod1),invariant(inv4)],true),po('C_m0','Invariant  preservation',[event(release_rod1),invariant(inv5)],true),po('C_m0','Invariant  preservation',[event(release_rod1),invariant(inv6)],true),po('C_m0','Invariant  preservation',[event(release_rod1),invariant(inv7)],true),po('C_m0','Invariant  preservation',[event(release_rod1),invariant(inv8)],true),po('C_m0','Invariant  preservation',[event(release_rod1),invariant(inv9)],true),po('C_m0','Invariant  preservation',[event(release_rod1),invariant(inv10)],true),po('C_m0','Invariant  preservation',[event(release_rod1),invariant(inv11)],true),po('C_m0','Invariant  preservation',[event(release_rod1),invariant(inv12)],true),po('C_m0','Invariant  preservation',[event(release_rod1),invariant(inv13)],true),po('C_m0','Invariant  preservation',[event(release_rod1),invariant(inv14)],true),po('C_m0','Theorem',[guard(grd2),event(release_rod2)],true),po('C_m0','Invariant  preservation',[event(release_rod2),invariant(inv1)],true),po('C_m0','Invariant  preservation',[event(release_rod2),invariant(inv2)],true),po('C_m0','Invariant  preservation',[event(release_rod2),invariant(inv3)],true),po('C_m0','Invariant  preservation',[event(release_rod2),invariant(inv4)],true),po('C_m0','Invariant  preservation',[event(release_rod2),invariant(inv5)],true),po('C_m0','Invariant  preservation',[event(release_rod2),invariant(inv6)],true),po('C_m0','Invariant  preservation',[event(release_rod2),invariant(inv7)],true),po('C_m0','Invariant  preservation',[event(release_rod2),invariant(inv8)],true),po('C_m0','Invariant  preservation',[event(release_rod2),invariant(inv9)],true),po('C_m0','Invariant  preservation',[event(release_rod2),invariant(inv10)],true),po('C_m0','Invariant  preservation',[event(release_rod2),invariant(inv11)],true),po('C_m0','Invariant  preservation',[event(release_rod2),invariant(inv12)],true),po('C_m0','Invariant  preservation',[event(release_rod2),invariant(inv13)],true),po('C_m0','Invariant  preservation',[event(release_rod2),invariant(inv14)],true)],_Error)).