diff --git a/Train_B_Book/train_1_beebook.prob2project b/Train_B_Book/train_1_beebook.prob2project
index 46087fa22275636567a8ea854b14fc25404d36f2..b14f3a20fe44e86d489e3a13cd70de456646fd79 100644
--- a/Train_B_Book/train_1_beebook.prob2project
+++ b/Train_B_Book/train_1_beebook.prob2project
@@ -55,13 +55,31 @@
       "simulation": null,
       "visBVisualisation": "train1.json",
       "historyChartItems": []
+    },
+    {
+      "name": "train_4_POR_mch",
+      "description": "",
+      "location": "train_4_POR_mch.eventb",
+      "lastUsedPreferenceName": "default",
+      "requirements": [],
+      "ltlFormulas": [],
+      "ltlPatterns": [],
+      "symbolicCheckingFormulas": [],
+      "symbolicAnimationFormulas": [],
+      "simulationItems": [],
+      "testCases": [],
+      "traces": [],
+      "modelcheckingItems": [],
+      "simulation": null,
+      "visBVisualisation": "train.json",
+      "historyChartItems": []
     }
   ],
   "preferences": [],
   "metadata": {
     "fileType": "Project",
     "formatVersion": 20,
-    "savedAt": "2022-02-01T16:13:48.000636Z",
+    "savedAt": "2022-02-03T11:33:15.308065Z",
     "creator": "User",
     "proB2KernelVersion": "3.15.0",
     "proBCliVersion": null,
diff --git a/Train_B_Book/train_4_POR_mch.eventb b/Train_B_Book/train_4_POR_mch.eventb
new file mode 100644
index 0000000000000000000000000000000000000000..637d076bdf3136525caa4df43d51526551b041d0
--- /dev/null
+++ b/Train_B_Book/train_4_POR_mch.eventb
@@ -0,0 +1,2 @@
+package(load_event_b_project([event_b_model(none,train_4_POR,[sees(none,[train_ctx0,train_ctx1,train_ctx2,train_ctx0_beebook,train_ctx1_beebook,train_ctx2_beebook]),refines(none,train_4),variables(none,[identifier(none,resrt),identifier(none,'OCC'),identifier(none,resbl),identifier(none,'GRN'),identifier(none,frm),identifier(none,'TRK'),identifier(none,'LBT'),identifier(none,rsrtbl)]),invariant(none,[]),theorems(none,[]),events(none,[event(rodinpos(train_4_POR,'INITIALISATION','_fnB_kIdnEeOcUOZ5WAG6MB'),'INITIALISATION',ordinary(none),['INITIALISATION'],[],[],[],[assign(rodinpos(train_4_POR,act1,internal_act1),[identifier(none,resrt)],[typeof(none,empty_set(none),pow_subset(none,identifier(none,'ROUTES')))]),assign(rodinpos(train_4_POR,act2,internal_act2),[identifier(none,resbl)],[typeof(none,empty_set(none),pow_subset(none,identifier(none,'BLOCKS')))]),assign(rodinpos(train_4_POR,act3,internal_act3),[identifier(none,rsrtbl)],[typeof(none,empty_set(none),pow_subset(none,cartesian_product(none,identifier(none,'BLOCKS'),identifier(none,'ROUTES'))))]),assign(rodinpos(train_4_POR,act4,internal_act4),[identifier(none,'OCC')],[typeof(none,empty_set(none),pow_subset(none,identifier(none,'BLOCKS')))]),assign(rodinpos(train_4_POR,act5,internal_element1),[identifier(none,'TRK')],[typeof(none,empty_set(none),pow_subset(none,cartesian_product(none,identifier(none,'BLOCKS'),identifier(none,'BLOCKS'))))]),assign(rodinpos(train_4_POR,act6,internal_element2),[identifier(none,frm)],[typeof(none,empty_set(none),pow_subset(none,identifier(none,'ROUTES')))]),assign(rodinpos(train_4_POR,act7,internal_element3),[identifier(none,'LBT')],[typeof(none,empty_set(none),pow_subset(none,identifier(none,'BLOCKS')))]),assign(rodinpos(train_4_POR,act8,internal_element4),[identifier(none,'GRN')],[typeof(none,empty_set(none),pow_subset(none,identifier(none,'S')))])],[]),event(rodinpos(train_4_POR,route_reservation,'_fnB_kIdnEeOcUOZ5WAG6MC'),route_reservation,ordinary(none),[route_reservation],[identifier(rodinpos(train_4_POR,[],internal_element1),r)],[not_member(rodinpos(train_4_POR,grd1,internal_element1),identifier(none,r),identifier(none,resrt)),equal(rodinpos(train_4_POR,grd2,internal_element2),intersection(none,image(none,reverse(none,identifier(none,rtbl)),set_extension(none,[identifier(none,r)])),identifier(none,resbl)),typeof(none,empty_set(none),pow_subset(none,identifier(none,'BLOCKS')))),equal(rodinpos(train_4_POR,'POR_route_freeing_impossible','_2AMecZSjEeOwFZMDEzeIXg'),set_subtraction(none,identifier(none,resrt),range(none,identifier(none,rsrtbl))),typeof(none,empty_set(none),pow_subset(none,identifier(none,'ROUTES'))))],[],[assign(rodinpos(train_4_POR,act1,internal_element1),[identifier(none,resrt)],[union(none,identifier(none,resrt),set_extension(none,[identifier(none,r)]))]),assign(rodinpos(train_4_POR,act2,internal_element2),[identifier(none,rsrtbl)],[union(none,identifier(none,rsrtbl),range_restriction(none,identifier(none,rtbl),set_extension(none,[identifier(none,r)])))]),assign(rodinpos(train_4_POR,act3,internal_element3),[identifier(none,resbl)],[union(none,identifier(none,resbl),image(none,reverse(none,identifier(none,rtbl)),set_extension(none,[identifier(none,r)])))])],[]),event(rodinpos(train_4_POR,route_freeing,'_fnB_kIdnEeOcUOZ5WAG6MD'),route_freeing,ordinary(none),[route_freeing],[identifier(rodinpos(train_4_POR,[],internal_element1),r)],[member(rodinpos(train_4_POR,grd1,internal_element1),identifier(none,r),set_subtraction(none,identifier(none,resrt),range(none,identifier(none,rsrtbl))))],[],[assign(rodinpos(train_4_POR,act1,internal_element1),[identifier(none,resrt)],[set_subtraction(none,identifier(none,resrt),set_extension(none,[identifier(none,r)]))]),assign(rodinpos(train_4_POR,act2,internal_element2),[identifier(none,frm)],[set_subtraction(none,identifier(none,frm),set_extension(none,[identifier(none,r)]))])],[]),event(rodinpos(train_4_POR,'FRONT_MOVE_1','_fnB_kIdnEeOcUOZ5WAG6ME'),'FRONT_MOVE_1',ordinary(none),['FRONT_MOVE_1'],[identifier(rodinpos(train_4_POR,[],internal_element1),b)],[member(rodinpos(train_4_POR,grd1,internal_element1),identifier(none,b),domain(none,identifier(none,'SIG'))),member(rodinpos(train_4_POR,grd2,internal_element2),function(none,identifier(none,'SIG'),[identifier(none,b)]),identifier(none,'GRN')),equal(rodinpos(train_4_POR,'POR_route_freeing_impossible','_2ANFgJSjEeOwFZMDEzeIXg'),set_subtraction(none,identifier(none,resrt),range(none,identifier(none,rsrtbl))),typeof(none,empty_set(none),pow_subset(none,identifier(none,'ROUTES'))))],[],[assign(rodinpos(train_4_POR,act1,internal_element1),[identifier(none,'OCC')],[union(none,identifier(none,'OCC'),set_extension(none,[identifier(none,b)]))]),assign(rodinpos(train_4_POR,act2,internal_element2),[identifier(none,'LBT')],[union(none,identifier(none,'LBT'),set_extension(none,[identifier(none,b)]))]),assign(rodinpos(train_4_POR,act3,internal_element3),[identifier(none,'GRN')],[set_subtraction(none,identifier(none,'GRN'),set_extension(none,[function(none,identifier(none,'SIG'),[identifier(none,b)])]))])],[]),event(rodinpos(train_4_POR,'FRONT_MOVE_2','_fnB_kIdnEeOcUOZ5WAG6MF'),'FRONT_MOVE_2',ordinary(none),['FRONT_MOVE_2'],[identifier(rodinpos(train_4_POR,[],internal_element1),b)],[member(rodinpos(train_4_POR,grd1,internal_element1),identifier(none,b),identifier(none,'OCC')),member(rodinpos(train_4_POR,grd2,internal_element2),identifier(none,b),domain(none,identifier(none,'TRK'))),not_member(rodinpos(train_4_POR,grd3,internal_element3),function(none,identifier(none,'TRK'),[identifier(none,b)]),identifier(none,'OCC')),equal(rodinpos(train_4_POR,'POR_route_freeing_impossible','_2ANFgZSjEeOwFZMDEzeIXg'),set_subtraction(none,identifier(none,resrt),range(none,identifier(none,rsrtbl))),typeof(none,empty_set(none),pow_subset(none,identifier(none,'ROUTES'))))],[],[assign(rodinpos(train_4_POR,act1,internal_element1),[identifier(none,'OCC')],[union(none,identifier(none,'OCC'),set_extension(none,[function(none,identifier(none,'TRK'),[identifier(none,b)])]))])],[]),event(rodinpos(train_4_POR,'BACK_MOVE_1','_fnB_kIdnEeOcUOZ5WAG6MG'),'BACK_MOVE_1',ordinary(none),['BACK_MOVE_1'],[identifier(rodinpos(train_4_POR,[],internal_element1),b)],[member(rodinpos(train_4_POR,grd1,internal_element1),identifier(none,b),identifier(none,'LBT')),not_member(rodinpos(train_4_POR,grd2,internal_element2),identifier(none,b),domain(none,identifier(none,'TRK'))),equal(rodinpos(train_4_POR,'POR_route_freeing_impossible','_2ANskJSjEeOwFZMDEzeIXg'),set_subtraction(none,identifier(none,resrt),range(none,identifier(none,rsrtbl))),typeof(none,empty_set(none),pow_subset(none,identifier(none,'ROUTES'))))],[],[assign(rodinpos(train_4_POR,act1,internal_element1),[identifier(none,'OCC')],[set_subtraction(none,identifier(none,'OCC'),set_extension(none,[identifier(none,b)]))]),assign(rodinpos(train_4_POR,act2,internal_element2),[identifier(none,rsrtbl)],[domain_subtraction(none,set_extension(none,[identifier(none,b)]),identifier(none,rsrtbl))]),assign(rodinpos(train_4_POR,act3,internal_element3),[identifier(none,resbl)],[set_subtraction(none,identifier(none,resbl),set_extension(none,[identifier(none,b)]))]),assign(rodinpos(train_4_POR,act4,internal_element4),[identifier(none,'LBT')],[set_subtraction(none,identifier(none,'LBT'),set_extension(none,[identifier(none,b)]))])],[]),event(rodinpos(train_4_POR,'BACK_MOVE_2','_fnB_kIdnEeOcUOZ5WAG6MH'),'BACK_MOVE_2',ordinary(none),['BACK_MOVE_2'],[identifier(rodinpos(train_4_POR,[],internal_element1),b)],[member(rodinpos(train_4_POR,grd1,internal_element1),identifier(none,b),identifier(none,'LBT')),member(rodinpos(train_4_POR,grd2,internal_element2),identifier(none,b),domain(none,identifier(none,'TRK'))),member(rodinpos(train_4_POR,grd3,internal_element3),function(none,identifier(none,'TRK'),[identifier(none,b)]),identifier(none,'OCC')),equal(rodinpos(train_4_POR,'POR_route_freeing_impossible','_2ANskZSjEeOwFZMDEzeIXg'),set_subtraction(none,identifier(none,resrt),range(none,identifier(none,rsrtbl))),typeof(none,empty_set(none),pow_subset(none,identifier(none,'ROUTES'))))],[],[assign(rodinpos(train_4_POR,act1,internal_element1),[identifier(none,'OCC')],[set_subtraction(none,identifier(none,'OCC'),set_extension(none,[identifier(none,b)]))]),assign(rodinpos(train_4_POR,act2,internal_element2),[identifier(none,rsrtbl)],[domain_subtraction(none,set_extension(none,[identifier(none,b)]),identifier(none,rsrtbl))]),assign(rodinpos(train_4_POR,act3,internal_element3),[identifier(none,resbl)],[set_subtraction(none,identifier(none,resbl),set_extension(none,[identifier(none,b)]))]),assign(rodinpos(train_4_POR,act4,internal_element4),[identifier(none,'LBT')],[union(none,set_subtraction(none,identifier(none,'LBT'),set_extension(none,[identifier(none,b)])),set_extension(none,[function(none,identifier(none,'TRK'),[identifier(none,b)])]))])],[]),event(rodinpos(train_4_POR,point_positionning,'_fnB_kIdnEeOcUOZ5WAG6MI'),point_positionning,ordinary(none),[point_positionning],[identifier(rodinpos(train_4_POR,[],internal_element1),r)],[member(rodinpos(train_4_POR,grd1,internal_element1),identifier(none,r),set_subtraction(none,identifier(none,resrt),identifier(none,frm))),equal(rodinpos(train_4_POR,'POR_route_freeing_impossible','_2ANskpSjEeOwFZMDEzeIXg'),set_subtraction(none,identifier(none,resrt),range(none,identifier(none,rsrtbl))),typeof(none,empty_set(none),pow_subset(none,identifier(none,'ROUTES'))))],[],[assign(rodinpos(train_4_POR,act1,internal_element1),[identifier(none,'TRK')],[union(none,range_subtraction(none,domain_subtraction(none,domain(none,function(none,identifier(none,nxt),[identifier(none,r)])),identifier(none,'TRK')),range(none,function(none,identifier(none,nxt),[identifier(none,r)]))),function(none,identifier(none,nxt),[identifier(none,r)]))])],[]),event(rodinpos(train_4_POR,route_formation,'_fnB_kIdnEeOcUOZ5WAG6MJ'),route_formation,ordinary(none),[route_formation],[identifier(rodinpos(train_4_POR,[],'\''),r)],[member(rodinpos(train_4_POR,grd1,'('),identifier(none,r),set_subtraction(none,identifier(none,resrt),identifier(none,frm))),equal(rodinpos(train_4_POR,grd2,')'),domain_restriction(none,image(none,reverse(none,identifier(none,rsrtbl)),set_extension(none,[identifier(none,r)])),function(none,identifier(none,nxt),[identifier(none,r)])),domain_restriction(none,image(none,reverse(none,identifier(none,rsrtbl)),set_extension(none,[identifier(none,r)])),identifier(none,'TRK'))),equal(rodinpos(train_4_POR,'POR_route_freeing_impossible','_2AOToJSjEeOwFZMDEzeIXg'),set_subtraction(none,identifier(none,resrt),range(none,identifier(none,rsrtbl))),typeof(none,empty_set(none),pow_subset(none,identifier(none,'ROUTES'))))],[],[assign(rodinpos(train_4_POR,act1,'*'),[identifier(none,frm)],[union(none,identifier(none,frm),set_extension(none,[identifier(none,r)]))]),assign(rodinpos(train_4_POR,act2,'+'),[identifier(none,'GRN')],[union(none,identifier(none,'GRN'),set_extension(none,[function(none,identifier(none,'SIG'),[function(none,identifier(none,fst),[identifier(none,r)])])]))])],[])])]),event_b_model(none,train_4,[sees(none,[train_ctx0,train_ctx1,train_ctx2]),refines(none,train_3),variables(none,[identifier(none,resrt),identifier(none,'OCC'),identifier(none,resbl),identifier(none,'GRN'),identifier(none,frm),identifier(none,'TRK'),identifier(none,'LBT'),identifier(none,rsrtbl)]),invariant(none,[member(rodinpos(train_4,inv1,internal_element1I),intersection(none,union(none,identifier(none,lft),identifier(none,rht)),union(none,identifier(none,'TRK'),reverse(none,identifier(none,'TRK')))),partial_function(none,identifier(none,blpt),identifier(none,'BLOCKS')))]),theorems(none,[]),events(none,[event(rodinpos(train_4,'INITIALISATION',internal_evt1),'INITIALISATION',ordinary(none),['INITIALISATION'],[],[],[],[assign(rodinpos(train_4,act1,internal_act1),[identifier(none,resrt)],[typeof(none,empty_set(none),pow_subset(none,identifier(none,'ROUTES')))]),assign(rodinpos(train_4,act2,internal_act2),[identifier(none,resbl)],[typeof(none,empty_set(none),pow_subset(none,identifier(none,'BLOCKS')))]),assign(rodinpos(train_4,act3,internal_act3),[identifier(none,rsrtbl)],[typeof(none,empty_set(none),pow_subset(none,cartesian_product(none,identifier(none,'BLOCKS'),identifier(none,'ROUTES'))))]),assign(rodinpos(train_4,act4,internal_act4),[identifier(none,'OCC')],[typeof(none,empty_set(none),pow_subset(none,identifier(none,'BLOCKS')))]),assign(rodinpos(train_4,act5,internal_element1),[identifier(none,'TRK')],[typeof(none,empty_set(none),pow_subset(none,cartesian_product(none,identifier(none,'BLOCKS'),identifier(none,'BLOCKS'))))]),assign(rodinpos(train_4,act6,internal_element2),[identifier(none,frm)],[typeof(none,empty_set(none),pow_subset(none,identifier(none,'ROUTES')))]),assign(rodinpos(train_4,act7,internal_element3),[identifier(none,'LBT')],[typeof(none,empty_set(none),pow_subset(none,identifier(none,'BLOCKS')))]),assign(rodinpos(train_4,act8,internal_element4),[identifier(none,'GRN')],[typeof(none,empty_set(none),pow_subset(none,identifier(none,'S')))])],[]),event(rodinpos(train_4,route_reservation,internal_element1),route_reservation,ordinary(none),[route_reservation],[identifier(rodinpos(train_4,[],internal_element1),r)],[not_member(rodinpos(train_4,grd1,internal_element1),identifier(none,r),identifier(none,resrt)),equal(rodinpos(train_4,grd2,internal_element2),intersection(none,image(none,reverse(none,identifier(none,rtbl)),set_extension(none,[identifier(none,r)])),identifier(none,resbl)),typeof(none,empty_set(none),pow_subset(none,identifier(none,'BLOCKS'))))],[],[assign(rodinpos(train_4,act1,internal_element1),[identifier(none,resrt)],[union(none,identifier(none,resrt),set_extension(none,[identifier(none,r)]))]),assign(rodinpos(train_4,act2,internal_element2),[identifier(none,rsrtbl)],[union(none,identifier(none,rsrtbl),range_restriction(none,identifier(none,rtbl),set_extension(none,[identifier(none,r)])))]),assign(rodinpos(train_4,act3,internal_element3),[identifier(none,resbl)],[union(none,identifier(none,resbl),image(none,reverse(none,identifier(none,rtbl)),set_extension(none,[identifier(none,r)])))])],[]),event(rodinpos(train_4,route_freeing,internal_element2),route_freeing,ordinary(none),[route_freeing],[identifier(rodinpos(train_4,[],internal_element1),r)],[member(rodinpos(train_4,grd1,internal_element1),identifier(none,r),set_subtraction(none,identifier(none,resrt),range(none,identifier(none,rsrtbl))))],[],[assign(rodinpos(train_4,act1,internal_element1),[identifier(none,resrt)],[set_subtraction(none,identifier(none,resrt),set_extension(none,[identifier(none,r)]))]),assign(rodinpos(train_4,act2,internal_element2),[identifier(none,frm)],[set_subtraction(none,identifier(none,frm),set_extension(none,[identifier(none,r)]))])],[]),event(rodinpos(train_4,'FRONT_MOVE_1',internal_element3),'FRONT_MOVE_1',ordinary(none),['FRONT_MOVE_1'],[identifier(rodinpos(train_4,[],internal_element1),b)],[member(rodinpos(train_4,grd1,internal_element1),identifier(none,b),domain(none,identifier(none,'SIG'))),member(rodinpos(train_4,grd2,internal_element2),function(none,identifier(none,'SIG'),[identifier(none,b)]),identifier(none,'GRN'))],[],[assign(rodinpos(train_4,act1,internal_element1),[identifier(none,'OCC')],[union(none,identifier(none,'OCC'),set_extension(none,[identifier(none,b)]))]),assign(rodinpos(train_4,act2,internal_element2),[identifier(none,'LBT')],[union(none,identifier(none,'LBT'),set_extension(none,[identifier(none,b)]))]),assign(rodinpos(train_4,act3,internal_element3),[identifier(none,'GRN')],[set_subtraction(none,identifier(none,'GRN'),set_extension(none,[function(none,identifier(none,'SIG'),[identifier(none,b)])]))])],[]),event(rodinpos(train_4,'FRONT_MOVE_2',internal_element4),'FRONT_MOVE_2',ordinary(none),['FRONT_MOVE_2'],[identifier(rodinpos(train_4,[],internal_element1),b)],[member(rodinpos(train_4,grd1,internal_element1),identifier(none,b),identifier(none,'OCC')),member(rodinpos(train_4,grd2,internal_element2),identifier(none,b),domain(none,identifier(none,'TRK'))),not_member(rodinpos(train_4,grd3,internal_element3),function(none,identifier(none,'TRK'),[identifier(none,b)]),identifier(none,'OCC'))],[],[assign(rodinpos(train_4,act1,internal_element1),[identifier(none,'OCC')],[union(none,identifier(none,'OCC'),set_extension(none,[function(none,identifier(none,'TRK'),[identifier(none,b)])]))])],[]),event(rodinpos(train_4,'BACK_MOVE_1',internal_element5),'BACK_MOVE_1',ordinary(none),['BACK_MOVE_1'],[identifier(rodinpos(train_4,[],internal_element1),b)],[member(rodinpos(train_4,grd1,internal_element1),identifier(none,b),identifier(none,'LBT')),not_member(rodinpos(train_4,grd2,internal_element2),identifier(none,b),domain(none,identifier(none,'TRK')))],[],[assign(rodinpos(train_4,act1,internal_element1),[identifier(none,'OCC')],[set_subtraction(none,identifier(none,'OCC'),set_extension(none,[identifier(none,b)]))]),assign(rodinpos(train_4,act2,internal_element2),[identifier(none,rsrtbl)],[domain_subtraction(none,set_extension(none,[identifier(none,b)]),identifier(none,rsrtbl))]),assign(rodinpos(train_4,act3,internal_element3),[identifier(none,resbl)],[set_subtraction(none,identifier(none,resbl),set_extension(none,[identifier(none,b)]))]),assign(rodinpos(train_4,act4,internal_element4),[identifier(none,'LBT')],[set_subtraction(none,identifier(none,'LBT'),set_extension(none,[identifier(none,b)]))])],[]),event(rodinpos(train_4,'BACK_MOVE_2',internal_element6),'BACK_MOVE_2',ordinary(none),['BACK_MOVE_2'],[identifier(rodinpos(train_4,[],internal_element1),b)],[member(rodinpos(train_4,grd1,internal_element1),identifier(none,b),identifier(none,'LBT')),member(rodinpos(train_4,grd2,internal_element2),identifier(none,b),domain(none,identifier(none,'TRK'))),member(rodinpos(train_4,grd3,internal_element3),function(none,identifier(none,'TRK'),[identifier(none,b)]),identifier(none,'OCC'))],[],[assign(rodinpos(train_4,act1,internal_element1),[identifier(none,'OCC')],[set_subtraction(none,identifier(none,'OCC'),set_extension(none,[identifier(none,b)]))]),assign(rodinpos(train_4,act2,internal_element2),[identifier(none,rsrtbl)],[domain_subtraction(none,set_extension(none,[identifier(none,b)]),identifier(none,rsrtbl))]),assign(rodinpos(train_4,act3,internal_element3),[identifier(none,resbl)],[set_subtraction(none,identifier(none,resbl),set_extension(none,[identifier(none,b)]))]),assign(rodinpos(train_4,act4,internal_element4),[identifier(none,'LBT')],[union(none,set_subtraction(none,identifier(none,'LBT'),set_extension(none,[identifier(none,b)])),set_extension(none,[function(none,identifier(none,'TRK'),[identifier(none,b)])]))])],[]),event(rodinpos(train_4,point_positionning,internal_element7),point_positionning,ordinary(none),[point_positionning],[identifier(rodinpos(train_4,[],internal_element1),r)],[member(rodinpos(train_4,grd1,internal_element1),identifier(none,r),set_subtraction(none,identifier(none,resrt),identifier(none,frm)))],[],[assign(rodinpos(train_4,act1,internal_element1),[identifier(none,'TRK')],[union(none,range_subtraction(none,domain_subtraction(none,domain(none,function(none,identifier(none,nxt),[identifier(none,r)])),identifier(none,'TRK')),range(none,function(none,identifier(none,nxt),[identifier(none,r)]))),function(none,identifier(none,nxt),[identifier(none,r)]))])],[]),event(rodinpos(train_4,route_formation,internal_refinesMachine2),route_formation,ordinary(none),[route_formation],[identifier(rodinpos(train_4,[],'\''),r)],[member(rodinpos(train_4,grd1,'('),identifier(none,r),set_subtraction(none,identifier(none,resrt),identifier(none,frm))),equal(rodinpos(train_4,grd2,')'),domain_restriction(none,image(none,reverse(none,identifier(none,rsrtbl)),set_extension(none,[identifier(none,r)])),function(none,identifier(none,nxt),[identifier(none,r)])),domain_restriction(none,image(none,reverse(none,identifier(none,rsrtbl)),set_extension(none,[identifier(none,r)])),identifier(none,'TRK')))],[],[assign(rodinpos(train_4,act1,'*'),[identifier(none,frm)],[union(none,identifier(none,frm),set_extension(none,[identifier(none,r)]))]),assign(rodinpos(train_4,act2,'+'),[identifier(none,'GRN')],[union(none,identifier(none,'GRN'),set_extension(none,[function(none,identifier(none,'SIG'),[function(none,identifier(none,fst),[identifier(none,r)])])]))])],[])])]),event_b_model(none,train_3,[sees(none,[train_ctx0,train_ctx1]),refines(none,train_2),variables(none,[identifier(none,resrt),identifier(none,'OCC'),identifier(none,resbl),identifier(none,'GRN'),identifier(none,frm),identifier(none,'TRK'),identifier(none,'LBT'),identifier(none,rsrtbl)]),invariant(none,[subset(rodinpos(train_3,inv1,internal_element1I),identifier(none,'GRN'),identifier(none,'S')),equal(rodinpos(train_3,inv2,internal_element2I),image(none,identifier(none,'SIG'),image(none,identifier(none,fst),identifier(none,rdy))),identifier(none,'GRN'))]),theorems(none,[member(rodinpos(train_3,thm1,internal_element1T),domain_restriction(none,identifier(none,rdy),identifier(none,fst)),total_injection(none,identifier(none,rdy),identifier(none,'BLOCKS')))]),events(none,[event(rodinpos(train_3,'INITIALISATION',internal_evt1),'INITIALISATION',ordinary(none),['INITIALISATION'],[],[],[],[assign(rodinpos(train_3,act1,internal_act1),[identifier(none,resrt)],[typeof(none,empty_set(none),pow_subset(none,identifier(none,'ROUTES')))]),assign(rodinpos(train_3,act2,internal_act2),[identifier(none,resbl)],[typeof(none,empty_set(none),pow_subset(none,identifier(none,'BLOCKS')))]),assign(rodinpos(train_3,act3,internal_act3),[identifier(none,rsrtbl)],[typeof(none,empty_set(none),pow_subset(none,cartesian_product(none,identifier(none,'BLOCKS'),identifier(none,'ROUTES'))))]),assign(rodinpos(train_3,act4,internal_act4),[identifier(none,'OCC')],[typeof(none,empty_set(none),pow_subset(none,identifier(none,'BLOCKS')))]),assign(rodinpos(train_3,act5,internal_element1),[identifier(none,'TRK')],[typeof(none,empty_set(none),pow_subset(none,cartesian_product(none,identifier(none,'BLOCKS'),identifier(none,'BLOCKS'))))]),assign(rodinpos(train_3,act6,internal_element2),[identifier(none,frm)],[typeof(none,empty_set(none),pow_subset(none,identifier(none,'ROUTES')))]),assign(rodinpos(train_3,act7,internal_element3),[identifier(none,'LBT')],[typeof(none,empty_set(none),pow_subset(none,identifier(none,'BLOCKS')))]),assign(rodinpos(train_3,act8,internal_element4),[identifier(none,'GRN')],[typeof(none,empty_set(none),pow_subset(none,identifier(none,'S')))])],[]),event(rodinpos(train_3,route_reservation,internal_element1),route_reservation,ordinary(none),[route_reservation],[identifier(rodinpos(train_3,[],internal_element1),r)],[not_member(rodinpos(train_3,grd1,internal_element1),identifier(none,r),identifier(none,resrt)),equal(rodinpos(train_3,grd2,internal_element2),intersection(none,image(none,reverse(none,identifier(none,rtbl)),set_extension(none,[identifier(none,r)])),identifier(none,resbl)),typeof(none,empty_set(none),pow_subset(none,identifier(none,'BLOCKS'))))],[],[assign(rodinpos(train_3,act1,internal_element1),[identifier(none,resrt)],[union(none,identifier(none,resrt),set_extension(none,[identifier(none,r)]))]),assign(rodinpos(train_3,act2,internal_element2),[identifier(none,rsrtbl)],[union(none,identifier(none,rsrtbl),range_restriction(none,identifier(none,rtbl),set_extension(none,[identifier(none,r)])))]),assign(rodinpos(train_3,act3,internal_element3),[identifier(none,resbl)],[union(none,identifier(none,resbl),image(none,reverse(none,identifier(none,rtbl)),set_extension(none,[identifier(none,r)])))])],[]),event(rodinpos(train_3,route_freeing,internal_element2),route_freeing,ordinary(none),[route_freeing],[identifier(rodinpos(train_3,[],internal_element1),r)],[member(rodinpos(train_3,grd1,internal_element1),identifier(none,r),set_subtraction(none,identifier(none,resrt),range(none,identifier(none,rsrtbl))))],[],[assign(rodinpos(train_3,act1,internal_element1),[identifier(none,resrt)],[set_subtraction(none,identifier(none,resrt),set_extension(none,[identifier(none,r)]))]),assign(rodinpos(train_3,act2,internal_element2),[identifier(none,frm)],[set_subtraction(none,identifier(none,frm),set_extension(none,[identifier(none,r)]))])],[]),event(rodinpos(train_3,'FRONT_MOVE_1',internal_element3),'FRONT_MOVE_1',ordinary(none),['FRONT_MOVE_1'],[identifier(rodinpos(train_3,[],internal_element1),b)],[member(rodinpos(train_3,grd1,internal_element1),identifier(none,b),domain(none,identifier(none,'SIG'))),member(rodinpos(train_3,grd2,internal_element2),function(none,identifier(none,'SIG'),[identifier(none,b)]),identifier(none,'GRN'))],[],[assign(rodinpos(train_3,act1,internal_element1),[identifier(none,'OCC')],[union(none,identifier(none,'OCC'),set_extension(none,[identifier(none,b)]))]),assign(rodinpos(train_3,act2,internal_element2),[identifier(none,'LBT')],[union(none,identifier(none,'LBT'),set_extension(none,[identifier(none,b)]))]),assign(rodinpos(train_3,act3,internal_element3),[identifier(none,'GRN')],[set_subtraction(none,identifier(none,'GRN'),set_extension(none,[function(none,identifier(none,'SIG'),[identifier(none,b)])]))])],[witness(none,identifier(none,r),conjunct(rodinpos(train_3,r,internal_wit1),member(none,identifier(none,r),identifier(none,rdy)),equal(none,function(none,identifier(none,fst),[identifier(none,r)]),identifier(none,b))))]),event(rodinpos(train_3,'FRONT_MOVE_2',internal_element4),'FRONT_MOVE_2',ordinary(none),['FRONT_MOVE_2'],[identifier(rodinpos(train_3,[],internal_element1),b)],[member(rodinpos(train_3,grd1,internal_element1),identifier(none,b),identifier(none,'OCC')),member(rodinpos(train_3,grd2,internal_element2),identifier(none,b),domain(none,identifier(none,'TRK'))),not_member(rodinpos(train_3,grd3,internal_element3),function(none,identifier(none,'TRK'),[identifier(none,b)]),identifier(none,'OCC'))],[],[assign(rodinpos(train_3,act1,internal_element1),[identifier(none,'OCC')],[union(none,identifier(none,'OCC'),set_extension(none,[function(none,identifier(none,'TRK'),[identifier(none,b)])]))])],[]),event(rodinpos(train_3,'BACK_MOVE_1',internal_element5),'BACK_MOVE_1',ordinary(none),['BACK_MOVE_1'],[identifier(rodinpos(train_3,[],internal_element1),b)],[member(rodinpos(train_3,grd1,internal_element1),identifier(none,b),identifier(none,'LBT')),not_member(rodinpos(train_3,grd2,internal_element2),identifier(none,b),domain(none,identifier(none,'TRK')))],[],[assign(rodinpos(train_3,act1,internal_element1),[identifier(none,'OCC')],[set_subtraction(none,identifier(none,'OCC'),set_extension(none,[identifier(none,b)]))]),assign(rodinpos(train_3,act2,internal_element2),[identifier(none,rsrtbl)],[domain_subtraction(none,set_extension(none,[identifier(none,b)]),identifier(none,rsrtbl))]),assign(rodinpos(train_3,act3,internal_element3),[identifier(none,resbl)],[set_subtraction(none,identifier(none,resbl),set_extension(none,[identifier(none,b)]))]),assign(rodinpos(train_3,act4,internal_element4),[identifier(none,'LBT')],[set_subtraction(none,identifier(none,'LBT'),set_extension(none,[identifier(none,b)]))])],[]),event(rodinpos(train_3,'BACK_MOVE_2',internal_element6),'BACK_MOVE_2',ordinary(none),['BACK_MOVE_2'],[identifier(rodinpos(train_3,[],internal_element1),b)],[member(rodinpos(train_3,grd1,internal_element1),identifier(none,b),identifier(none,'LBT')),member(rodinpos(train_3,grd2,internal_element2),identifier(none,b),domain(none,identifier(none,'TRK'))),member(rodinpos(train_3,grd3,internal_element3),function(none,identifier(none,'TRK'),[identifier(none,b)]),identifier(none,'OCC'))],[],[assign(rodinpos(train_3,act1,internal_element1),[identifier(none,'OCC')],[set_subtraction(none,identifier(none,'OCC'),set_extension(none,[identifier(none,b)]))]),assign(rodinpos(train_3,act2,internal_element2),[identifier(none,rsrtbl)],[domain_subtraction(none,set_extension(none,[identifier(none,b)]),identifier(none,rsrtbl))]),assign(rodinpos(train_3,act3,internal_element3),[identifier(none,resbl)],[set_subtraction(none,identifier(none,resbl),set_extension(none,[identifier(none,b)]))]),assign(rodinpos(train_3,act4,internal_element4),[identifier(none,'LBT')],[union(none,set_subtraction(none,identifier(none,'LBT'),set_extension(none,[identifier(none,b)])),set_extension(none,[function(none,identifier(none,'TRK'),[identifier(none,b)])]))])],[]),event(rodinpos(train_3,point_positionning,internal_element7),point_positionning,ordinary(none),[point_positionning],[identifier(rodinpos(train_3,[],internal_element1),r)],[member(rodinpos(train_3,grd1,internal_element1),identifier(none,r),set_subtraction(none,identifier(none,resrt),identifier(none,frm)))],[],[assign(rodinpos(train_3,act1,internal_element1),[identifier(none,'TRK')],[union(none,range_subtraction(none,domain_subtraction(none,domain(none,function(none,identifier(none,nxt),[identifier(none,r)])),identifier(none,'TRK')),range(none,function(none,identifier(none,nxt),[identifier(none,r)]))),function(none,identifier(none,nxt),[identifier(none,r)]))])],[]),event(rodinpos(train_3,route_formation,internal_refinesMachine2),route_formation,ordinary(none),[route_formation],[identifier(rodinpos(train_3,[],'\''),r)],[member(rodinpos(train_3,grd1,'('),identifier(none,r),set_subtraction(none,identifier(none,resrt),identifier(none,frm))),equal(rodinpos(train_3,grd2,')'),domain_restriction(none,image(none,reverse(none,identifier(none,rsrtbl)),set_extension(none,[identifier(none,r)])),function(none,identifier(none,nxt),[identifier(none,r)])),domain_restriction(none,image(none,reverse(none,identifier(none,rsrtbl)),set_extension(none,[identifier(none,r)])),identifier(none,'TRK')))],[],[assign(rodinpos(train_3,act1,'*'),[identifier(none,frm)],[union(none,identifier(none,frm),set_extension(none,[identifier(none,r)]))]),assign(rodinpos(train_3,act2,'+'),[identifier(none,'GRN')],[union(none,identifier(none,'GRN'),set_extension(none,[function(none,identifier(none,'SIG'),[function(none,identifier(none,fst),[identifier(none,r)])])]))])],[])])]),event_b_model(none,train_2,[sees(none,[train_ctx0]),refines(none,train_1),variables(none,[identifier(none,rdy),identifier(none,resrt),identifier(none,'OCC'),identifier(none,resbl),identifier(none,frm),identifier(none,'TRK'),identifier(none,'LBT'),identifier(none,rsrtbl)]),invariant(none,[subset(rodinpos(train_2,inv4,internal_refinesMachine3),identifier(none,rdy),identifier(none,frm)),forall(rodinpos(train_2,inv2,internal_element2I),[identifier(none,r)],implication(none,conjunct(none,member(none,identifier(none,r),identifier(none,'ROUTES')),member(none,identifier(none,r),identifier(none,rdy))),equal(none,range_restriction(none,identifier(none,rtbl),set_extension(none,[identifier(none,r)])),range_restriction(none,identifier(none,rsrtbl),set_extension(none,[identifier(none,r)]))))),forall(rodinpos(train_2,inv3,internal_element3I),[identifier(none,r)],implication(none,conjunct(none,member(none,identifier(none,r),identifier(none,'ROUTES')),member(none,identifier(none,r),identifier(none,rdy))),equal(none,intersection(none,domain(none,range_restriction(none,identifier(none,rtbl),set_extension(none,[identifier(none,r)]))),identifier(none,'OCC')),typeof(none,empty_set(none),pow_subset(none,identifier(none,'BLOCKS'))))))]),theorems(none,[]),events(none,[event(rodinpos(train_2,'INITIALISATION',internal_evt1),'INITIALISATION',ordinary(none),['INITIALISATION'],[],[],[],[assign(rodinpos(train_2,act1,internal_act1),[identifier(none,resrt)],[typeof(none,empty_set(none),pow_subset(none,identifier(none,'ROUTES')))]),assign(rodinpos(train_2,act2,internal_act2),[identifier(none,resbl)],[typeof(none,empty_set(none),pow_subset(none,identifier(none,'BLOCKS')))]),assign(rodinpos(train_2,act3,internal_act3),[identifier(none,rsrtbl)],[typeof(none,empty_set(none),pow_subset(none,cartesian_product(none,identifier(none,'BLOCKS'),identifier(none,'ROUTES'))))]),assign(rodinpos(train_2,act4,internal_act4),[identifier(none,'OCC')],[typeof(none,empty_set(none),pow_subset(none,identifier(none,'BLOCKS')))]),assign(rodinpos(train_2,act5,internal_element1),[identifier(none,'TRK')],[typeof(none,empty_set(none),pow_subset(none,cartesian_product(none,identifier(none,'BLOCKS'),identifier(none,'BLOCKS'))))]),assign(rodinpos(train_2,act6,internal_element2),[identifier(none,frm)],[typeof(none,empty_set(none),pow_subset(none,identifier(none,'ROUTES')))]),assign(rodinpos(train_2,act7,internal_element3),[identifier(none,'LBT')],[typeof(none,empty_set(none),pow_subset(none,identifier(none,'BLOCKS')))]),assign(rodinpos(train_2,act8,internal_element4),[identifier(none,rdy)],[typeof(none,empty_set(none),pow_subset(none,identifier(none,'ROUTES')))])],[]),event(rodinpos(train_2,route_reservation,internal_element1),route_reservation,ordinary(none),[route_reservation],[identifier(rodinpos(train_2,[],internal_element1),r)],[not_member(rodinpos(train_2,grd1,internal_element1),identifier(none,r),identifier(none,resrt)),equal(rodinpos(train_2,grd2,internal_element2),intersection(none,image(none,reverse(none,identifier(none,rtbl)),set_extension(none,[identifier(none,r)])),identifier(none,resbl)),typeof(none,empty_set(none),pow_subset(none,identifier(none,'BLOCKS'))))],[],[assign(rodinpos(train_2,act1,internal_element1),[identifier(none,resrt)],[union(none,identifier(none,resrt),set_extension(none,[identifier(none,r)]))]),assign(rodinpos(train_2,act2,internal_element2),[identifier(none,rsrtbl)],[union(none,identifier(none,rsrtbl),range_restriction(none,identifier(none,rtbl),set_extension(none,[identifier(none,r)])))]),assign(rodinpos(train_2,act3,internal_element3),[identifier(none,resbl)],[union(none,identifier(none,resbl),image(none,reverse(none,identifier(none,rtbl)),set_extension(none,[identifier(none,r)])))])],[]),event(rodinpos(train_2,route_freeing,internal_element2),route_freeing,ordinary(none),[route_freeing],[identifier(rodinpos(train_2,[],internal_element1),r)],[member(rodinpos(train_2,grd1,internal_element1),identifier(none,r),set_subtraction(none,identifier(none,resrt),range(none,identifier(none,rsrtbl))))],[],[assign(rodinpos(train_2,act1,internal_element1),[identifier(none,resrt)],[set_subtraction(none,identifier(none,resrt),set_extension(none,[identifier(none,r)]))]),assign(rodinpos(train_2,act2,internal_element2),[identifier(none,frm)],[set_subtraction(none,identifier(none,frm),set_extension(none,[identifier(none,r)]))])],[]),event(rodinpos(train_2,'FRONT_MOVE_1',internal_element3),'FRONT_MOVE_1',ordinary(none),['FRONT_MOVE_1'],[identifier(rodinpos(train_2,[],internal_element1),r)],[member(rodinpos(train_2,grd1,internal_element1),identifier(none,r),identifier(none,rdy)),equal(rodinpos(train_2,grd2,internal_element2),function(none,identifier(none,rsrtbl),[function(none,identifier(none,fst),[identifier(none,r)])]),identifier(none,r))],[],[assign(rodinpos(train_2,act1,internal_element1),[identifier(none,'OCC')],[union(none,identifier(none,'OCC'),set_extension(none,[function(none,identifier(none,fst),[identifier(none,r)])]))]),assign(rodinpos(train_2,act2,internal_element2),[identifier(none,'LBT')],[union(none,identifier(none,'LBT'),set_extension(none,[function(none,identifier(none,fst),[identifier(none,r)])]))]),assign(rodinpos(train_2,act3,internal_element3),[identifier(none,rdy)],[set_subtraction(none,identifier(none,rdy),set_extension(none,[identifier(none,r)]))])],[]),event(rodinpos(train_2,'FRONT_MOVE_2',internal_element4),'FRONT_MOVE_2',ordinary(none),['FRONT_MOVE_2'],[identifier(rodinpos(train_2,[],internal_element1),b)],[member(rodinpos(train_2,grd1,internal_element1),identifier(none,b),identifier(none,'OCC')),member(rodinpos(train_2,grd2,internal_element2),identifier(none,b),domain(none,identifier(none,'TRK'))),not_member(rodinpos(train_2,grd3,internal_element3),function(none,identifier(none,'TRK'),[identifier(none,b)]),identifier(none,'OCC'))],[],[assign(rodinpos(train_2,act1,internal_element1),[identifier(none,'OCC')],[union(none,identifier(none,'OCC'),set_extension(none,[function(none,identifier(none,'TRK'),[identifier(none,b)])]))])],[]),event(rodinpos(train_2,'BACK_MOVE_1',internal_element5),'BACK_MOVE_1',ordinary(none),['BACK_MOVE_1'],[identifier(rodinpos(train_2,[],internal_element1),b)],[member(rodinpos(train_2,grd1,internal_element1),identifier(none,b),identifier(none,'LBT')),not_member(rodinpos(train_2,grd2,internal_element2),identifier(none,b),domain(none,identifier(none,'TRK')))],[],[assign(rodinpos(train_2,act1,internal_element1),[identifier(none,'OCC')],[set_subtraction(none,identifier(none,'OCC'),set_extension(none,[identifier(none,b)]))]),assign(rodinpos(train_2,act2,internal_element2),[identifier(none,rsrtbl)],[domain_subtraction(none,set_extension(none,[identifier(none,b)]),identifier(none,rsrtbl))]),assign(rodinpos(train_2,act3,internal_element3),[identifier(none,resbl)],[set_subtraction(none,identifier(none,resbl),set_extension(none,[identifier(none,b)]))]),assign(rodinpos(train_2,act4,internal_element4),[identifier(none,'LBT')],[set_subtraction(none,identifier(none,'LBT'),set_extension(none,[identifier(none,b)]))])],[]),event(rodinpos(train_2,'BACK_MOVE_2',internal_element6),'BACK_MOVE_2',ordinary(none),['BACK_MOVE_2'],[identifier(rodinpos(train_2,[],internal_element1),b)],[member(rodinpos(train_2,grd1,internal_element1),identifier(none,b),identifier(none,'LBT')),member(rodinpos(train_2,grd2,internal_element2),identifier(none,b),domain(none,identifier(none,'TRK'))),member(rodinpos(train_2,grd3,internal_element3),function(none,identifier(none,'TRK'),[identifier(none,b)]),identifier(none,'OCC'))],[],[assign(rodinpos(train_2,act1,internal_element1),[identifier(none,'OCC')],[set_subtraction(none,identifier(none,'OCC'),set_extension(none,[identifier(none,b)]))]),assign(rodinpos(train_2,act2,internal_element2),[identifier(none,rsrtbl)],[domain_subtraction(none,set_extension(none,[identifier(none,b)]),identifier(none,rsrtbl))]),assign(rodinpos(train_2,act3,internal_element3),[identifier(none,resbl)],[set_subtraction(none,identifier(none,resbl),set_extension(none,[identifier(none,b)]))]),assign(rodinpos(train_2,act4,internal_element4),[identifier(none,'LBT')],[union(none,set_subtraction(none,identifier(none,'LBT'),set_extension(none,[identifier(none,b)])),set_extension(none,[function(none,identifier(none,'TRK'),[identifier(none,b)])]))])],[]),event(rodinpos(train_2,point_positionning,internal_evt2),point_positionning,ordinary(none),[point_positionning],[identifier(rodinpos(train_2,[],internal_element1),r)],[member(rodinpos(train_2,grd1,internal_element1),identifier(none,r),set_subtraction(none,identifier(none,resrt),identifier(none,frm)))],[],[assign(rodinpos(train_2,act1,internal_element1),[identifier(none,'TRK')],[union(none,range_subtraction(none,domain_subtraction(none,domain(none,function(none,identifier(none,nxt),[identifier(none,r)])),identifier(none,'TRK')),range(none,function(none,identifier(none,nxt),[identifier(none,r)]))),function(none,identifier(none,nxt),[identifier(none,r)]))])],[]),event(rodinpos(train_2,route_formation,internal_refinesMachine2),route_formation,ordinary(none),[route_formation],[identifier(rodinpos(train_2,[],'\''),r)],[member(rodinpos(train_2,grd1,'('),identifier(none,r),set_subtraction(none,identifier(none,resrt),identifier(none,frm))),equal(rodinpos(train_2,grd2,')'),domain_restriction(none,image(none,reverse(none,identifier(none,rsrtbl)),set_extension(none,[identifier(none,r)])),function(none,identifier(none,nxt),[identifier(none,r)])),domain_restriction(none,image(none,reverse(none,identifier(none,rsrtbl)),set_extension(none,[identifier(none,r)])),identifier(none,'TRK')))],[],[assign(rodinpos(train_2,act1,'*'),[identifier(none,frm)],[union(none,identifier(none,frm),set_extension(none,[identifier(none,r)]))]),assign(rodinpos(train_2,act3,'-'),[identifier(none,rdy)],[union(none,identifier(none,rdy),set_extension(none,[identifier(none,r)]))])],[])])]),event_b_model(none,train_1,[sees(none,[train_ctx0]),refines(none,train_0),variables(none,[identifier(none,resrt),identifier(none,'OCC'),identifier(none,resbl),identifier(none,frm),identifier(none,'TRK'),identifier(none,'LBT'),identifier(none,rsrtbl)]),invariant(none,[member(rodinpos(train_1,inv1,internal_element1I),identifier(none,'TRK'),partial_injection(none,identifier(none,'BLOCKS'),identifier(none,'BLOCKS'))),subset(rodinpos(train_1,inv2,internal_element2I),identifier(none,frm),identifier(none,resrt)),subset(rodinpos(train_1,inv3,internal_element3I),image(none,identifier(none,rsrtbl),identifier(none,'OCC')),identifier(none,frm)),forall(rodinpos(train_1,inv4,internal_element4I),[identifier(none,r)],implication(none,conjunct(none,member(none,identifier(none,r),identifier(none,'ROUTES')),member(none,identifier(none,r),set_subtraction(none,identifier(none,resrt),identifier(none,frm)))),equal(none,range_restriction(none,identifier(none,rtbl),set_extension(none,[identifier(none,r)])),range_restriction(none,identifier(none,rsrtbl),set_extension(none,[identifier(none,r)]))))),forall(rodinpos(train_1,inv5,internal_element5I),[identifier(none,x),identifier(none,y)],implication(none,conjunct(none,member(none,identifier(none,x),identifier(none,'BLOCKS')),conjunct(none,member(none,identifier(none,y),identifier(none,'BLOCKS')),member(none,couple(none,[identifier(none,x),identifier(none,y)]),identifier(none,'TRK')))),exists(none,[identifier(none,r)],conjunct(none,member(none,identifier(none,r),identifier(none,'ROUTES')),conjunct(none,member(none,identifier(none,r),identifier(none,'ROUTES')),member(none,couple(none,[identifier(none,x),identifier(none,y)]),function(none,identifier(none,nxt),[identifier(none,r)]))))))),forall(rodinpos(train_1,inv6,internal_element6I),[identifier(none,r)],implication(none,conjunct(none,member(none,identifier(none,r),identifier(none,'ROUTES')),member(none,identifier(none,r),identifier(none,frm))),equal(none,domain_restriction(none,image(none,reverse(none,identifier(none,rsrtbl)),set_extension(none,[identifier(none,r)])),function(none,identifier(none,nxt),[identifier(none,r)])),domain_restriction(none,image(none,reverse(none,identifier(none,rsrtbl)),set_extension(none,[identifier(none,r)])),identifier(none,'TRK'))))),subset(rodinpos(train_1,inv7,internal_element7I),identifier(none,'LBT'),identifier(none,'OCC')),forall(rodinpos(train_1,inv8,internal_element8I),[identifier(none,a),identifier(none,b)],implication(none,conjunct(none,member(none,identifier(none,a),identifier(none,'BLOCKS')),conjunct(none,member(none,identifier(none,b),identifier(none,'BLOCKS')),conjunct(none,member(none,identifier(none,b),identifier(none,'LBT')),conjunct(none,member(none,identifier(none,b),range(none,function(none,identifier(none,nxt),[function(none,identifier(none,rsrtbl),[identifier(none,b)])]))),conjunct(none,equal(none,identifier(none,a),function(none,reverse(none,function(none,identifier(none,nxt),[function(none,identifier(none,rsrtbl),[identifier(none,b)])])),[identifier(none,b)])),member(none,identifier(none,a),domain(none,identifier(none,rsrtbl)))))))),not_equal(none,function(none,identifier(none,rsrtbl),[identifier(none,a)]),function(none,identifier(none,rsrtbl),[identifier(none,b)]))))]),theorems(none,[forall(rodinpos(train_1,thm1,internal_element1T),[identifier(none,b)],implication(none,conjunct(none,member(none,identifier(none,b),identifier(none,'BLOCKS')),conjunct(none,member(none,identifier(none,b),identifier(none,'OCC')),member(none,identifier(none,b),domain(none,identifier(none,'TRK'))))),equal(none,function(none,function(none,identifier(none,nxt),[function(none,identifier(none,rsrtbl),[identifier(none,b)])]),[identifier(none,b)]),function(none,identifier(none,'TRK'),[identifier(none,b)])))),equal(rodinpos(train_1,thm2,internal_element8K),intersection(none,range(none,identifier(none,lst)),set_subtraction(none,domain(none,identifier(none,'TRK')),range(none,identifier(none,fst)))),typeof(none,empty_set(none),pow_subset(none,identifier(none,'BLOCKS')))),equal(rodinpos(train_1,thm3,internal_element8L),intersection(none,range(none,identifier(none,fst)),set_subtraction(none,range(none,identifier(none,'TRK')),range(none,identifier(none,lst)))),typeof(none,empty_set(none),pow_subset(none,identifier(none,'BLOCKS'))))]),events(none,[event(rodinpos(train_1,'INITIALISATION',internal_evt1),'INITIALISATION',ordinary(none),['INITIALISATION'],[],[],[],[assign(rodinpos(train_1,act1,internal_act1),[identifier(none,resrt)],[typeof(none,empty_set(none),pow_subset(none,identifier(none,'ROUTES')))]),assign(rodinpos(train_1,act2,internal_act2),[identifier(none,resbl)],[typeof(none,empty_set(none),pow_subset(none,identifier(none,'BLOCKS')))]),assign(rodinpos(train_1,act3,internal_act3),[identifier(none,rsrtbl)],[typeof(none,empty_set(none),pow_subset(none,cartesian_product(none,identifier(none,'BLOCKS'),identifier(none,'ROUTES'))))]),assign(rodinpos(train_1,act4,internal_act4),[identifier(none,'OCC')],[typeof(none,empty_set(none),pow_subset(none,identifier(none,'BLOCKS')))]),assign(rodinpos(train_1,act5,internal_element1),[identifier(none,'TRK')],[typeof(none,empty_set(none),pow_subset(none,cartesian_product(none,identifier(none,'BLOCKS'),identifier(none,'BLOCKS'))))]),assign(rodinpos(train_1,act6,internal_element2),[identifier(none,frm)],[typeof(none,empty_set(none),pow_subset(none,identifier(none,'ROUTES')))]),assign(rodinpos(train_1,act7,internal_element3),[identifier(none,'LBT')],[typeof(none,empty_set(none),pow_subset(none,identifier(none,'BLOCKS')))])],[]),event(rodinpos(train_1,route_reservation,internal_element1),route_reservation,ordinary(none),[route_reservation],[identifier(rodinpos(train_1,[],internal_element1),r)],[not_member(rodinpos(train_1,grd1,internal_element1),identifier(none,r),identifier(none,resrt)),equal(rodinpos(train_1,grd2,internal_element2),intersection(none,image(none,reverse(none,identifier(none,rtbl)),set_extension(none,[identifier(none,r)])),identifier(none,resbl)),typeof(none,empty_set(none),pow_subset(none,identifier(none,'BLOCKS'))))],[],[assign(rodinpos(train_1,act1,internal_element1),[identifier(none,resrt)],[union(none,identifier(none,resrt),set_extension(none,[identifier(none,r)]))]),assign(rodinpos(train_1,act2,internal_element2),[identifier(none,rsrtbl)],[union(none,identifier(none,rsrtbl),range_restriction(none,identifier(none,rtbl),set_extension(none,[identifier(none,r)])))]),assign(rodinpos(train_1,act3,internal_element3),[identifier(none,resbl)],[union(none,identifier(none,resbl),image(none,reverse(none,identifier(none,rtbl)),set_extension(none,[identifier(none,r)])))])],[]),event(rodinpos(train_1,route_freeing,internal_element2),route_freeing,ordinary(none),[route_freeing],[identifier(rodinpos(train_1,[],internal_element1),r)],[member(rodinpos(train_1,grd1,internal_element1),identifier(none,r),set_subtraction(none,identifier(none,resrt),range(none,identifier(none,rsrtbl))))],[],[assign(rodinpos(train_1,act1,internal_element1),[identifier(none,resrt)],[set_subtraction(none,identifier(none,resrt),set_extension(none,[identifier(none,r)]))]),assign(rodinpos(train_1,act2,internal_element2),[identifier(none,frm)],[set_subtraction(none,identifier(none,frm),set_extension(none,[identifier(none,r)]))])],[]),event(rodinpos(train_1,'FRONT_MOVE_1',internal_element3),'FRONT_MOVE_1',ordinary(none),['FRONT_MOVE_1'],[identifier(rodinpos(train_1,[],'_QdStMIdPEeOSfLkA9HaR6w'),r)],[member(rodinpos(train_1,grd1,'_QdStMYdPEeOSfLkA9HaR6w'),identifier(none,r),identifier(none,frm)),member(rodinpos(train_1,grd2,'_QdStModPEeOSfLkA9HaR6w'),function(none,identifier(none,fst),[identifier(none,r)]),set_subtraction(none,identifier(none,resbl),identifier(none,'OCC'))),equal(rodinpos(train_1,grd3,'_QdTUQIdPEeOSfLkA9HaR6w'),function(none,identifier(none,rsrtbl),[function(none,identifier(none,fst),[identifier(none,r)])]),identifier(none,r))],[],[assign(rodinpos(train_1,act1,'_QdTUQYdPEeOSfLkA9HaR6w'),[identifier(none,'OCC')],[union(none,identifier(none,'OCC'),set_extension(none,[function(none,identifier(none,fst),[identifier(none,r)])]))]),assign(rodinpos(train_1,act2,internal_element2),[identifier(none,'LBT')],[union(none,identifier(none,'LBT'),set_extension(none,[function(none,identifier(none,fst),[identifier(none,r)])]))])],[]),event(rodinpos(train_1,'FRONT_MOVE_2',internal_element4),'FRONT_MOVE_2',ordinary(none),['FRONT_MOVE_2'],[identifier(rodinpos(train_1,[],internal_element1),b)],[member(rodinpos(train_1,grd1,internal_element1),identifier(none,b),identifier(none,'OCC')),member(rodinpos(train_1,grd2,internal_element2),identifier(none,b),domain(none,identifier(none,'TRK'))),not_member(rodinpos(train_1,grd3,internal_element3),function(none,identifier(none,'TRK'),[identifier(none,b)]),identifier(none,'OCC'))],[],[assign(rodinpos(train_1,act1,internal_element1),[identifier(none,'OCC')],[union(none,identifier(none,'OCC'),set_extension(none,[function(none,identifier(none,'TRK'),[identifier(none,b)])]))])],[witness(none,identifier(none,c),equal(rodinpos(train_1,c,internal_wit1),identifier(none,c),function(none,identifier(none,'TRK'),[identifier(none,b)])))]),event(rodinpos(train_1,'BACK_MOVE_1',internal_element5),'BACK_MOVE_1',ordinary(none),['BACK_MOVE'],[identifier(rodinpos(train_1,[],internal_element1),b)],[member(rodinpos(train_1,grd1,internal_element1),identifier(none,b),identifier(none,'LBT')),not_member(rodinpos(train_1,grd2,internal_element2),identifier(none,b),domain(none,identifier(none,'TRK')))],[],[assign(rodinpos(train_1,act1,internal_element1),[identifier(none,'OCC')],[set_subtraction(none,identifier(none,'OCC'),set_extension(none,[identifier(none,b)]))]),assign(rodinpos(train_1,act2,internal_element2),[identifier(none,rsrtbl)],[domain_subtraction(none,set_extension(none,[identifier(none,b)]),identifier(none,rsrtbl))]),assign(rodinpos(train_1,act3,internal_element3),[identifier(none,resbl)],[set_subtraction(none,identifier(none,resbl),set_extension(none,[identifier(none,b)]))]),assign(rodinpos(train_1,act4,internal_element4),[identifier(none,'LBT')],[set_subtraction(none,identifier(none,'LBT'),set_extension(none,[identifier(none,b)]))])],[witness(none,identifier(none,n),equal(rodinpos(train_1,n,internal_wit1),identifier(none,n),function(none,identifier(none,nxt),[function(none,identifier(none,rsrtbl),[identifier(none,b)])])))]),event(rodinpos(train_1,'BACK_MOVE_2',internal_element6),'BACK_MOVE_2',ordinary(none),['BACK_MOVE'],[identifier(rodinpos(train_1,[],internal_element1),b)],[member(rodinpos(train_1,grd1,internal_element1),identifier(none,b),identifier(none,'LBT')),member(rodinpos(train_1,grd2,internal_element2),identifier(none,b),domain(none,identifier(none,'TRK'))),member(rodinpos(train_1,grd3,internal_element3),function(none,identifier(none,'TRK'),[identifier(none,b)]),identifier(none,'OCC'))],[],[assign(rodinpos(train_1,act1,internal_element1),[identifier(none,'OCC')],[set_subtraction(none,identifier(none,'OCC'),set_extension(none,[identifier(none,b)]))]),assign(rodinpos(train_1,act2,internal_element2),[identifier(none,rsrtbl)],[domain_subtraction(none,set_extension(none,[identifier(none,b)]),identifier(none,rsrtbl))]),assign(rodinpos(train_1,act3,internal_element3),[identifier(none,resbl)],[set_subtraction(none,identifier(none,resbl),set_extension(none,[identifier(none,b)]))]),assign(rodinpos(train_1,act4,internal_element4),[identifier(none,'LBT')],[union(none,set_subtraction(none,identifier(none,'LBT'),set_extension(none,[identifier(none,b)])),set_extension(none,[function(none,identifier(none,'TRK'),[identifier(none,b)])]))])],[witness(none,identifier(none,n),equal(rodinpos(train_1,n,internal_wit1),identifier(none,n),function(none,identifier(none,nxt),[function(none,identifier(none,rsrtbl),[identifier(none,b)])])))]),event(rodinpos(train_1,point_positionning,internal_element7),point_positionning,ordinary(none),[],[identifier(rodinpos(train_1,[],internal_element1),r)],[member(rodinpos(train_1,grd1,internal_element1),identifier(none,r),set_subtraction(none,identifier(none,resrt),identifier(none,frm)))],[],[assign(rodinpos(train_1,act1,internal_element1),[identifier(none,'TRK')],[union(none,range_subtraction(none,domain_subtraction(none,domain(none,function(none,identifier(none,nxt),[identifier(none,r)])),identifier(none,'TRK')),range(none,function(none,identifier(none,nxt),[identifier(none,r)]))),function(none,identifier(none,nxt),[identifier(none,r)]))])],[]),event(rodinpos(train_1,route_formation,internal_element8J),route_formation,ordinary(none),[],[identifier(rodinpos(train_1,[],'\''),r)],[member(rodinpos(train_1,grd1,'('),identifier(none,r),set_subtraction(none,identifier(none,resrt),identifier(none,frm))),equal(rodinpos(train_1,grd2,')'),domain_restriction(none,image(none,reverse(none,identifier(none,rsrtbl)),set_extension(none,[identifier(none,r)])),function(none,identifier(none,nxt),[identifier(none,r)])),domain_restriction(none,image(none,reverse(none,identifier(none,rsrtbl)),set_extension(none,[identifier(none,r)])),identifier(none,'TRK')))],[],[assign(rodinpos(train_1,act1,'*'),[identifier(none,frm)],[union(none,identifier(none,frm),set_extension(none,[identifier(none,r)]))])],[])])]),event_b_model(none,train_0,[sees(none,[train_ctx0]),variables(none,[identifier(none,resrt),identifier(none,'OCC'),identifier(none,resbl),identifier(none,rsrtbl)]),invariant(none,[subset(rodinpos(train_0,inv1,internal_inv1I),identifier(none,resrt),identifier(none,'ROUTES')),subset(rodinpos(train_0,inv2,internal_inv2I),identifier(none,resbl),identifier(none,'BLOCKS')),member(rodinpos(train_0,inv3,internal_inv3I),identifier(none,rsrtbl),total_function(none,identifier(none,resbl),identifier(none,resrt))),subset(rodinpos(train_0,inv5,internal_inv5I),identifier(none,rsrtbl),identifier(none,rtbl)),subset(rodinpos(train_0,inv4,internal_inv4I),identifier(none,'OCC'),identifier(none,resbl)),forall(rodinpos(train_0,inv6,internal_element1I),[identifier(none,r)],implication(none,conjunct(none,member(none,identifier(none,r),identifier(none,'ROUTES')),member(none,identifier(none,r),identifier(none,'ROUTES'))),equal(none,intersection(none,image(none,function(none,identifier(none,nxt),[identifier(none,r)]),set_subtraction(none,image(none,reverse(none,identifier(none,rtbl)),set_extension(none,[identifier(none,r)])),image(none,reverse(none,identifier(none,rsrtbl)),set_extension(none,[identifier(none,r)])))),set_subtraction(none,image(none,reverse(none,identifier(none,rsrtbl)),set_extension(none,[identifier(none,r)])),identifier(none,'OCC'))),typeof(none,empty_set(none),pow_subset(none,identifier(none,'BLOCKS')))))),forall(rodinpos(train_0,inv7,internal_element2I),[identifier(none,r)],implication(none,conjunct(none,member(none,identifier(none,r),identifier(none,'ROUTES')),member(none,identifier(none,r),identifier(none,'ROUTES'))),subset(none,image(none,function(none,identifier(none,nxt),[identifier(none,r)]),image(none,reverse(none,identifier(none,rsrtbl)),set_extension(none,[identifier(none,r)]))),image(none,reverse(none,identifier(none,rsrtbl)),set_extension(none,[identifier(none,r)]))))),forall(rodinpos(train_0,inv8,internal_element3I),[identifier(none,r)],implication(none,conjunct(none,member(none,identifier(none,r),identifier(none,'ROUTES')),member(none,identifier(none,r),identifier(none,'ROUTES'))),subset(none,image(none,function(none,identifier(none,nxt),[identifier(none,r)]),set_subtraction(none,image(none,reverse(none,identifier(none,rsrtbl)),set_extension(none,[identifier(none,r)])),identifier(none,'OCC'))),set_subtraction(none,image(none,reverse(none,identifier(none,rsrtbl)),set_extension(none,[identifier(none,r)])),identifier(none,'OCC')))))]),theorems(none,[]),events(none,[event(rodinpos(train_0,'INITIALISATION',internal_evt1),'INITIALISATION',ordinary(none),[],[],[],[],[assign(rodinpos(train_0,act1,internal_act1),[identifier(none,resrt)],[typeof(none,empty_set(none),pow_subset(none,identifier(none,'ROUTES')))]),assign(rodinpos(train_0,act2,internal_act2),[identifier(none,resbl)],[typeof(none,empty_set(none),pow_subset(none,identifier(none,'BLOCKS')))]),assign(rodinpos(train_0,act3,internal_act3),[identifier(none,rsrtbl)],[typeof(none,empty_set(none),pow_subset(none,cartesian_product(none,identifier(none,'BLOCKS'),identifier(none,'ROUTES'))))]),assign(rodinpos(train_0,act4,internal_act4),[identifier(none,'OCC')],[typeof(none,empty_set(none),pow_subset(none,identifier(none,'BLOCKS')))])],[]),event(rodinpos(train_0,route_reservation,internal_element1),route_reservation,ordinary(none),[],[identifier(rodinpos(train_0,[],internal_element1),r)],[not_member(rodinpos(train_0,grd1,internal_element1),identifier(none,r),identifier(none,resrt)),equal(rodinpos(train_0,grd2,internal_element2),intersection(none,image(none,reverse(none,identifier(none,rtbl)),set_extension(none,[identifier(none,r)])),identifier(none,resbl)),typeof(none,empty_set(none),pow_subset(none,identifier(none,'BLOCKS'))))],[],[assign(rodinpos(train_0,act1,internal_element1),[identifier(none,resrt)],[union(none,identifier(none,resrt),set_extension(none,[identifier(none,r)]))]),assign(rodinpos(train_0,act2,internal_element2),[identifier(none,rsrtbl)],[union(none,identifier(none,rsrtbl),range_restriction(none,identifier(none,rtbl),set_extension(none,[identifier(none,r)])))]),assign(rodinpos(train_0,act3,internal_element3),[identifier(none,resbl)],[union(none,identifier(none,resbl),image(none,reverse(none,identifier(none,rtbl)),set_extension(none,[identifier(none,r)])))])],[]),event(rodinpos(train_0,route_freeing,internal_element2),route_freeing,ordinary(none),[],[identifier(rodinpos(train_0,[],internal_element1),r)],[member(rodinpos(train_0,grd1,internal_element1),identifier(none,r),set_subtraction(none,identifier(none,resrt),range(none,identifier(none,rsrtbl))))],[],[assign(rodinpos(train_0,act1,internal_element1),[identifier(none,resrt)],[set_subtraction(none,identifier(none,resrt),set_extension(none,[identifier(none,r)]))])],[]),event(rodinpos(train_0,'FRONT_MOVE_1',internal_element3),'FRONT_MOVE_1',ordinary(none),[],[identifier(rodinpos(train_0,[],internal_element1),r)],[member(rodinpos(train_0,grd1,internal_element1),identifier(none,r),identifier(none,resrt)),member(rodinpos(train_0,grd2,internal_element2),function(none,identifier(none,fst),[identifier(none,r)]),set_subtraction(none,identifier(none,resbl),identifier(none,'OCC'))),equal(rodinpos(train_0,grd3,internal_element3),function(none,identifier(none,rsrtbl),[function(none,identifier(none,fst),[identifier(none,r)])]),identifier(none,r))],[],[assign(rodinpos(train_0,act1,internal_element1),[identifier(none,'OCC')],[union(none,identifier(none,'OCC'),set_extension(none,[function(none,identifier(none,fst),[identifier(none,r)])]))])],[]),event(rodinpos(train_0,'FRONT_MOVE_2',internal_element4),'FRONT_MOVE_2',ordinary(none),[],[identifier(rodinpos(train_0,[],internal_element1),b),identifier(rodinpos(train_0,[],internal_element2),c)],[member(rodinpos(train_0,grd1,internal_element1),identifier(none,b),identifier(none,'OCC')),not_member(rodinpos(train_0,grd2,internal_element2),identifier(none,c),identifier(none,'OCC')),member(rodinpos(train_0,grd3,internal_element3),couple(none,[identifier(none,b),identifier(none,c)]),function(none,identifier(none,nxt),[function(none,identifier(none,rsrtbl),[identifier(none,b)])]))],[],[assign(rodinpos(train_0,act1,internal_element1),[identifier(none,'OCC')],[union(none,identifier(none,'OCC'),set_extension(none,[identifier(none,c)]))])],[]),event(rodinpos(train_0,'BACK_MOVE',internal_element5),'BACK_MOVE',ordinary(none),[],[identifier(rodinpos(train_0,[],internal_element1),b),identifier(rodinpos(train_0,[],internal_element2),n)],[member(rodinpos(train_0,grd1,internal_element1),identifier(none,b),identifier(none,'OCC')),equal(rodinpos(train_0,grd2,internal_element2),identifier(none,n),function(none,identifier(none,nxt),[function(none,identifier(none,rsrtbl),[identifier(none,b)])])),implication(rodinpos(train_0,grd3,internal_element3),member(none,identifier(none,b),domain(none,identifier(none,n))),member(none,function(none,identifier(none,n),[identifier(none,b)]),identifier(none,'OCC'))),implication(rodinpos(train_0,grd4,internal_element4),conjunct(none,member(none,identifier(none,b),range(none,identifier(none,n))),member(none,function(none,reverse(none,identifier(none,n)),[identifier(none,b)]),domain(none,identifier(none,rsrtbl)))),not_equal(none,function(none,identifier(none,rsrtbl),[function(none,reverse(none,identifier(none,n)),[identifier(none,b)])]),function(none,identifier(none,rsrtbl),[identifier(none,b)])))],[],[assign(rodinpos(train_0,act1,internal_element1),[identifier(none,'OCC')],[set_subtraction(none,identifier(none,'OCC'),set_extension(none,[identifier(none,b)]))]),assign(rodinpos(train_0,act2,internal_element2),[identifier(none,rsrtbl)],[domain_subtraction(none,set_extension(none,[identifier(none,b)]),identifier(none,rsrtbl))]),assign(rodinpos(train_0,act3,internal_element3),[identifier(none,resbl)],[set_subtraction(none,identifier(none,resbl),set_extension(none,[identifier(none,b)]))])],[])])])],[event_b_context(none,train_ctx0,[extends(none,[]),constants(none,[identifier(none,rtbl),identifier(none,lst),identifier(none,nxt),identifier(none,fst)]),abstract_constants(none,[]),axioms(none,[member(rodinpos(train_ctx0,axm1,internal_axm1A),identifier(none,rtbl),relations(none,identifier(none,'BLOCKS'),identifier(none,'ROUTES'))),equal(rodinpos(train_ctx0,axm2,internal_axm2A),domain(none,identifier(none,rtbl)),identifier(none,'BLOCKS')),equal(rodinpos(train_ctx0,axm3,internal_axm3A),range(none,identifier(none,rtbl)),identifier(none,'ROUTES')),member(rodinpos(train_ctx0,axm4,internal_axm4A),identifier(none,nxt),total_function(none,identifier(none,'ROUTES'),partial_injection(none,identifier(none,'BLOCKS'),identifier(none,'BLOCKS')))),member(rodinpos(train_ctx0,axm5,internal_axm5A),identifier(none,fst),total_function(none,identifier(none,'ROUTES'),identifier(none,'BLOCKS'))),member(rodinpos(train_ctx0,axm6,internal_axm6A),identifier(none,lst),total_function(none,identifier(none,'ROUTES'),identifier(none,'BLOCKS'))),subset(rodinpos(train_ctx0,axm7,internal_axm7A),reverse(none,identifier(none,fst)),identifier(none,rtbl)),subset(rodinpos(train_ctx0,axm8,internal_axm8A),reverse(none,identifier(none,lst)),identifier(none,rtbl)),forall(rodinpos(train_ctx0,axm11,internal_axm11A),[identifier(none,r)],implication(none,conjunct(none,member(none,identifier(none,r),identifier(none,'ROUTES')),member(none,identifier(none,r),identifier(none,'ROUTES'))),not_equal(none,function(none,identifier(none,fst),[identifier(none,r)]),function(none,identifier(none,lst),[identifier(none,r)])))),forall(rodinpos(train_ctx0,axm10,internal_axm10A),[identifier(none,r)],implication(none,conjunct(none,member(none,identifier(none,r),identifier(none,'ROUTES')),member(none,identifier(none,r),identifier(none,'ROUTES'))),forall(none,[identifier(none,'S')],implication(none,conjunct(none,member(none,identifier(none,'S'),pow_subset(none,identifier(none,'BLOCKS'))),conjunct(none,subset(none,identifier(none,'S'),range(none,function(none,identifier(none,nxt),[identifier(none,r)]))),subset(none,identifier(none,'S'),image(none,function(none,identifier(none,nxt),[identifier(none,r)]),identifier(none,'S'))))),equal(none,identifier(none,'S'),typeof(none,empty_set(none),pow_subset(none,identifier(none,'BLOCKS')))))))),forall(rodinpos(train_ctx0,axm9,internal_axm9A),[identifier(none,r)],implication(none,conjunct(none,member(none,identifier(none,r),identifier(none,'ROUTES')),member(none,identifier(none,r),identifier(none,'ROUTES'))),member(none,function(none,identifier(none,nxt),[identifier(none,r)]),total_bijection(none,set_subtraction(none,image(none,reverse(none,identifier(none,rtbl)),set_extension(none,[identifier(none,r)])),set_extension(none,[function(none,identifier(none,lst),[identifier(none,r)])])),set_subtraction(none,image(none,reverse(none,identifier(none,rtbl)),set_extension(none,[identifier(none,r)])),set_extension(none,[function(none,identifier(none,fst),[identifier(none,r)])])))))),forall(rodinpos(train_ctx0,axm12,internal_axm12A),[identifier(none,r),identifier(none,s)],implication(none,conjunct(none,member(none,identifier(none,r),identifier(none,'ROUTES')),conjunct(none,member(none,identifier(none,s),identifier(none,'ROUTES')),conjunct(none,member(none,identifier(none,r),identifier(none,'ROUTES')),conjunct(none,member(none,identifier(none,s),identifier(none,'ROUTES')),not_equal(none,identifier(none,r),identifier(none,s)))))),not_member(none,function(none,identifier(none,fst),[identifier(none,r)]),set_subtraction(none,image(none,reverse(none,identifier(none,rtbl)),set_extension(none,[identifier(none,s)])),set_extension(none,[function(none,identifier(none,fst),[identifier(none,s)]),function(none,identifier(none,lst),[identifier(none,s)])]))))),forall(rodinpos(train_ctx0,axm13,internal_axm13A),[identifier(none,r),identifier(none,s)],implication(none,conjunct(none,member(none,identifier(none,r),identifier(none,'ROUTES')),conjunct(none,member(none,identifier(none,s),identifier(none,'ROUTES')),conjunct(none,member(none,identifier(none,r),identifier(none,'ROUTES')),conjunct(none,member(none,identifier(none,s),identifier(none,'ROUTES')),not_equal(none,identifier(none,r),identifier(none,s)))))),not_member(none,function(none,identifier(none,lst),[identifier(none,r)]),set_subtraction(none,image(none,reverse(none,identifier(none,rtbl)),set_extension(none,[identifier(none,s)])),set_extension(none,[function(none,identifier(none,fst),[identifier(none,s)]),function(none,identifier(none,lst),[identifier(none,s)])])))))]),theorems(none,[]),sets(none,[deferred_set(none,'ROUTES'),deferred_set(none,'BLOCKS')])]),event_b_context(none,train_ctx1,[extends(none,[train_ctx0]),constants(none,[identifier(none,'SIG')]),abstract_constants(none,[]),axioms(none,[member(rodinpos(train_ctx1,axm1,internal_axm1A),identifier(none,'SIG'),total_bijection(none,range(none,identifier(none,fst)),identifier(none,'S')))]),theorems(none,[]),sets(none,[deferred_set(none,'S')])]),event_b_context(none,train_ctx2,[extends(none,[train_ctx1]),constants(none,[identifier(none,rht),identifier(none,lft),identifier(none,blpt)]),abstract_constants(none,[]),axioms(none,[subset(rodinpos(train_ctx2,axm1,internal_axm1A),identifier(none,blpt),identifier(none,'BLOCKS')),member(rodinpos(train_ctx2,axm2,internal_axm2A),identifier(none,lft),total_function(none,identifier(none,blpt),identifier(none,'BLOCKS'))),member(rodinpos(train_ctx2,axm3,internal_axm3A),identifier(none,rht),total_function(none,identifier(none,blpt),identifier(none,'BLOCKS'))),equal(rodinpos(train_ctx2,axm4,internal_axm4A),intersection(none,identifier(none,lft),identifier(none,rht)),typeof(none,empty_set(none),pow_subset(none,cartesian_product(none,identifier(none,'BLOCKS'),identifier(none,'BLOCKS'))))),forall(rodinpos(train_ctx2,axm5,internal_axm5A),[identifier(none,r)],implication(none,conjunct(none,member(none,identifier(none,r),identifier(none,'ROUTES')),member(none,identifier(none,r),identifier(none,'ROUTES'))),member(none,intersection(none,union(none,identifier(none,lft),identifier(none,rht)),union(none,function(none,identifier(none,nxt),[identifier(none,r)]),reverse(none,function(none,identifier(none,nxt),[identifier(none,r)])))),partial_function(none,identifier(none,blpt),identifier(none,'BLOCKS'))))),equal(rodinpos(train_ctx2,axm6,internal_axm6A),intersection(none,identifier(none,blpt),range(none,identifier(none,fst))),typeof(none,empty_set(none),pow_subset(none,identifier(none,'BLOCKS')))),equal(rodinpos(train_ctx2,axm7,internal_axm7A),intersection(none,identifier(none,blpt),range(none,identifier(none,lst))),typeof(none,empty_set(none),pow_subset(none,identifier(none,'BLOCKS'))))]),theorems(none,[]),sets(none,[])]),event_b_context(none,train_ctx0_beebook,[extends(none,[train_ctx0]),constants(none,[identifier(none,'A'),identifier(none,'B'),identifier(none,'C'),identifier(none,'D'),identifier(none,'E'),identifier(none,'F'),identifier(none,'G'),identifier(none,'H'),identifier(none,'I'),identifier(none,'J'),identifier(none,'K'),identifier(none,'L'),identifier(none,'M'),identifier(none,'N'),identifier(none,'R10'),identifier(none,'R1'),identifier(none,'R2'),identifier(none,'R3'),identifier(none,'R4'),identifier(none,'R5'),identifier(none,'R6'),identifier(none,'R7'),identifier(none,'R8'),identifier(none,'R9')]),abstract_constants(none,[]),axioms(none,[partition(rodinpos(train_ctx0_beebook,axm44,'_uj5LAIdoEeOcUOZ5WAG6MA'),identifier(none,'BLOCKS'),[set_extension(none,[identifier(none,'A')]),set_extension(none,[identifier(none,'B')]),set_extension(none,[identifier(none,'C')]),set_extension(none,[identifier(none,'D')]),set_extension(none,[identifier(none,'E')]),set_extension(none,[identifier(none,'F')]),set_extension(none,[identifier(none,'G')]),set_extension(none,[identifier(none,'H')]),set_extension(none,[identifier(none,'I')]),set_extension(none,[identifier(none,'J')]),set_extension(none,[identifier(none,'K')]),set_extension(none,[identifier(none,'L')]),set_extension(none,[identifier(none,'M')]),set_extension(none,[identifier(none,'N')])]),partition(rodinpos(train_ctx0_beebook,axm45,'_uj5LAYdoEeOcUOZ5WAG6MA'),identifier(none,'ROUTES'),[set_extension(none,[identifier(none,'R1')]),set_extension(none,[identifier(none,'R2')]),set_extension(none,[identifier(none,'R3')]),set_extension(none,[identifier(none,'R4')]),set_extension(none,[identifier(none,'R5')]),set_extension(none,[identifier(none,'R6')]),set_extension(none,[identifier(none,'R7')]),set_extension(none,[identifier(none,'R8')]),set_extension(none,[identifier(none,'R9')]),set_extension(none,[identifier(none,'R10')])]),equal(rodinpos(train_ctx0_beebook,compute_rtbl_from_nxt,'_tx3w0YdrEeOYLZrGGNvfWA'),identifier(none,rtbl),event_b_comprehension_set(none,[identifier(none,b),identifier(none,r)],couple(none,[identifier(none,b),identifier(none,r)]),conjunct(none,member(none,identifier(none,b),identifier(none,'BLOCKS')),conjunct(none,member(none,identifier(none,r),identifier(none,'ROUTES')),conjunct(none,member(none,identifier(none,r),domain(none,identifier(none,nxt))),disjunct(none,member(none,identifier(none,b),domain(none,function(none,identifier(none,nxt),[identifier(none,r)]))),member(none,identifier(none,b),range(none,function(none,identifier(none,nxt),[identifier(none,r)]))))))))),equal(rodinpos(train_ctx0_beebook,axm40,'_uj5LA4doEeOcUOZ5WAG6MA'),identifier(none,nxt),set_extension(none,[couple(none,[identifier(none,'R1'),set_extension(none,[couple(none,[identifier(none,'L'),identifier(none,'A')]),couple(none,[identifier(none,'A'),identifier(none,'B')]),couple(none,[identifier(none,'B'),identifier(none,'C')])])]),couple(none,[identifier(none,'R2'),set_extension(none,[couple(none,[identifier(none,'L'),identifier(none,'A')]),couple(none,[identifier(none,'A'),identifier(none,'B')]),couple(none,[identifier(none,'B'),identifier(none,'D')]),couple(none,[identifier(none,'D'),identifier(none,'E')]),couple(none,[identifier(none,'E'),identifier(none,'F')]),couple(none,[identifier(none,'F'),identifier(none,'G')])])]),couple(none,[identifier(none,'R3'),set_extension(none,[couple(none,[identifier(none,'L'),identifier(none,'A')]),couple(none,[identifier(none,'A'),identifier(none,'B')]),couple(none,[identifier(none,'B'),identifier(none,'D')]),couple(none,[identifier(none,'D'),identifier(none,'K')]),couple(none,[identifier(none,'K'),identifier(none,'J')]),couple(none,[identifier(none,'J'),identifier(none,'N')])])]),couple(none,[identifier(none,'R4'),set_extension(none,[couple(none,[identifier(none,'M'),identifier(none,'H')]),couple(none,[identifier(none,'H'),identifier(none,'I')]),couple(none,[identifier(none,'I'),identifier(none,'K')]),couple(none,[identifier(none,'K'),identifier(none,'F')]),couple(none,[identifier(none,'F'),identifier(none,'G')])])]),couple(none,[identifier(none,'R5'),set_extension(none,[couple(none,[identifier(none,'M'),identifier(none,'H')]),couple(none,[identifier(none,'H'),identifier(none,'I')]),couple(none,[identifier(none,'I'),identifier(none,'J')]),couple(none,[identifier(none,'J'),identifier(none,'N')])])]),couple(none,[identifier(none,'R6'),set_extension(none,[couple(none,[identifier(none,'C'),identifier(none,'B')]),couple(none,[identifier(none,'B'),identifier(none,'A')]),couple(none,[identifier(none,'A'),identifier(none,'L')])])]),couple(none,[identifier(none,'R7'),set_extension(none,[couple(none,[identifier(none,'G'),identifier(none,'F')]),couple(none,[identifier(none,'F'),identifier(none,'E')]),couple(none,[identifier(none,'E'),identifier(none,'D')]),couple(none,[identifier(none,'D'),identifier(none,'B')]),couple(none,[identifier(none,'B'),identifier(none,'A')]),couple(none,[identifier(none,'A'),identifier(none,'L')])])]),couple(none,[identifier(none,'R8'),set_extension(none,[couple(none,[identifier(none,'N'),identifier(none,'J')]),couple(none,[identifier(none,'J'),identifier(none,'K')]),couple(none,[identifier(none,'K'),identifier(none,'D')]),couple(none,[identifier(none,'D'),identifier(none,'B')]),couple(none,[identifier(none,'B'),identifier(none,'A')]),couple(none,[identifier(none,'A'),identifier(none,'L')])])]),couple(none,[identifier(none,'R9'),set_extension(none,[couple(none,[identifier(none,'G'),identifier(none,'F')]),couple(none,[identifier(none,'F'),identifier(none,'K')]),couple(none,[identifier(none,'K'),identifier(none,'I')]),couple(none,[identifier(none,'I'),identifier(none,'H')]),couple(none,[identifier(none,'H'),identifier(none,'M')])])]),couple(none,[identifier(none,'R10'),set_extension(none,[couple(none,[identifier(none,'N'),identifier(none,'J')]),couple(none,[identifier(none,'J'),identifier(none,'I')]),couple(none,[identifier(none,'I'),identifier(none,'H')]),couple(none,[identifier(none,'H'),identifier(none,'M')])])])])),equal(rodinpos(train_ctx0_beebook,axm41,'_uj5LBIdoEeOcUOZ5WAG6MA'),identifier(none,fst),set_extension(none,[couple(none,[identifier(none,'R1'),identifier(none,'L')]),couple(none,[identifier(none,'R2'),identifier(none,'L')]),couple(none,[identifier(none,'R3'),identifier(none,'L')]),couple(none,[identifier(none,'R4'),identifier(none,'M')]),couple(none,[identifier(none,'R5'),identifier(none,'M')]),couple(none,[identifier(none,'R6'),identifier(none,'C')]),couple(none,[identifier(none,'R7'),identifier(none,'G')]),couple(none,[identifier(none,'R8'),identifier(none,'N')]),couple(none,[identifier(none,'R9'),identifier(none,'G')]),couple(none,[identifier(none,'R10'),identifier(none,'N')])])),equal(rodinpos(train_ctx0_beebook,axm42,'_uj5yEIdoEeOcUOZ5WAG6MA'),identifier(none,lst),set_extension(none,[couple(none,[identifier(none,'R1'),identifier(none,'C')]),couple(none,[identifier(none,'R2'),identifier(none,'G')]),couple(none,[identifier(none,'R3'),identifier(none,'N')]),couple(none,[identifier(none,'R4'),identifier(none,'G')]),couple(none,[identifier(none,'R5'),identifier(none,'N')]),couple(none,[identifier(none,'R6'),identifier(none,'L')]),couple(none,[identifier(none,'R7'),identifier(none,'L')]),couple(none,[identifier(none,'R8'),identifier(none,'L')]),couple(none,[identifier(none,'R9'),identifier(none,'M')]),couple(none,[identifier(none,'R10'),identifier(none,'M')])]))]),theorems(none,[]),sets(none,[])]),event_b_context(none,train_ctx1_beebook,[extends(none,[train_ctx1,train_ctx0_beebook]),constants(none,[identifier(none,'S1'),identifier(none,'S2'),identifier(none,'S3'),identifier(none,'S4'),identifier(none,'S5')]),abstract_constants(none,[]),axioms(none,[partition(rodinpos(train_ctx1_beebook,axm3,'_5Sf7YIdrEeOYLZrGGNvfWA'),identifier(none,'S'),[set_extension(none,[identifier(none,'S1')]),set_extension(none,[identifier(none,'S2')]),set_extension(none,[identifier(none,'S3')]),set_extension(none,[identifier(none,'S4')]),set_extension(none,[identifier(none,'S5')])]),equal(rodinpos(train_ctx1_beebook,axm4,'_5Sf7YYdrEeOYLZrGGNvfWA'),identifier(none,'SIG'),set_extension(none,[couple(none,[identifier(none,'L'),identifier(none,'S1')]),couple(none,[identifier(none,'M'),identifier(none,'S2')]),couple(none,[identifier(none,'N'),identifier(none,'S3')]),couple(none,[identifier(none,'C'),identifier(none,'S4')]),couple(none,[identifier(none,'G'),identifier(none,'S5')])]))]),theorems(none,[equal(rodinpos(train_ctx1_beebook,axm2,'_5SfUU4drEeOYLZrGGNvfWA'),card(none,identifier(none,'S')),integer(none,5))]),sets(none,[])]),event_b_context(none,train_ctx2_beebook,[extends(none,[train_ctx2,train_ctx1_beebook]),constants(none,[]),abstract_constants(none,[]),axioms(none,[equal(rodinpos(train_ctx2_beebook,prob_axm1,'_MRgjEodsEeOYLZrGGNvfWA'),identifier(none,blpt),set_extension(none,[identifier(none,'B'),identifier(none,'D'),identifier(none,'F'),identifier(none,'I'),identifier(none,'J')]))]),theorems(none,[]),sets(none,[])])],[exporter_version(3),po(train_ctx0,'Well-definedness of Axiom',[axiom(axm11)],true),po(train_ctx0,'Well-definedness of Axiom',[axiom(axm10)],true),po(train_ctx0,'Well-definedness of Axiom',[axiom(axm9)],true),po(train_ctx0,'Well-definedness of Axiom',[axiom(axm12)],true),po(train_ctx0,'Well-definedness of Axiom',[axiom(axm13)],true),po(train_ctx2,'Well-definedness of Axiom',[axiom(axm5)],true),po(train_ctx0_beebook,'Well-definedness of Axiom',[axiom(compute_rtbl_from_nxt)],false),po(train_ctx1_beebook,'Well-definedness of Theorem',[axiom(axm2)],false),po(train_ctx1_beebook,'Theorem',[axiom(axm2)],false),po(train_4,'Invariant  establishment',[event('INITIALISATION'),event('INITIALISATION'),invariant(inv1)],true),po(train_4,'Invariant  preservation',[event(point_positionning),event(point_positionning),invariant(inv1)],false),po(train_2,'Invariant  establishment',[event('INITIALISATION'),event('INITIALISATION'),invariant(inv4)],true),po(train_2,'Invariant  establishment',[event('INITIALISATION'),event('INITIALISATION'),invariant(inv2)],true),po(train_2,'Invariant  establishment',[event('INITIALISATION'),event('INITIALISATION'),invariant(inv3)],true),po(train_2,'Invariant  preservation',[event(route_reservation),event(route_reservation),invariant(inv2)],true),po(train_2,'Invariant  preservation',[event(route_freeing),event(route_freeing),invariant(inv4)],true),po(train_2,'Well-definedness of Guard',[guard(grd2),event('FRONT_MOVE_1')],false),po(train_2,'Invariant  preservation',[event('FRONT_MOVE_1'),event('FRONT_MOVE_1'),invariant(inv4)],true),po(train_2,'Invariant  preservation',[event('FRONT_MOVE_1'),event('FRONT_MOVE_1'),invariant(inv2)],true),po(train_2,'Invariant  preservation',[event('FRONT_MOVE_1'),event('FRONT_MOVE_1'),invariant(inv3)],false),po(train_2,'Guard strengthening (split)',[event('FRONT_MOVE_1'),guard(grd1),event('FRONT_MOVE_1'),event('FRONT_MOVE_1')],true),po(train_2,'Guard strengthening (split)',[event('FRONT_MOVE_1'),guard(grd2),event('FRONT_MOVE_1'),event('FRONT_MOVE_1')],false),po(train_2,'Invariant  preservation',[event('FRONT_MOVE_2'),event('FRONT_MOVE_2'),invariant(inv3)],false),po(train_2,'Invariant  preservation',[event('BACK_MOVE_1'),event('BACK_MOVE_1'),invariant(inv2)],false),po(train_2,'Invariant  preservation',[event('BACK_MOVE_1'),event('BACK_MOVE_1'),invariant(inv3)],true),po(train_2,'Invariant  preservation',[event('BACK_MOVE_2'),event('BACK_MOVE_2'),invariant(inv2)],false),po(train_2,'Invariant  preservation',[event('BACK_MOVE_2'),event('BACK_MOVE_2'),invariant(inv3)],true),po(train_2,'Invariant  preservation',[event(route_formation),event(route_formation),invariant(inv4)],true),po(train_2,'Invariant  preservation',[event(route_formation),event(route_formation),invariant(inv2)],false),po(train_2,'Invariant  preservation',[event(route_formation),event(route_formation),invariant(inv3)],false),po(train_1,'Well-definedness of Invariant',[invariant(inv5)],true),po(train_1,'Well-definedness of Invariant',[invariant(inv6)],true),po(train_1,'Well-definedness of Invariant',[invariant(inv8)],true),po(train_1,'Well-definedness of Theorem',[invariant(thm1)],false),po(train_1,'Theorem',[invariant(thm1)],false),po(train_1,'Theorem',[invariant(thm2)],false),po(train_1,'Theorem',[invariant(thm3)],false),po(train_1,'Invariant  establishment',[event('INITIALISATION'),event('INITIALISATION'),invariant(inv1)],true),po(train_1,'Invariant  establishment',[event('INITIALISATION'),event('INITIALISATION'),invariant(inv2)],true),po(train_1,'Invariant  establishment',[event('INITIALISATION'),event('INITIALISATION'),invariant(inv3)],true),po(train_1,'Invariant  establishment',[event('INITIALISATION'),event('INITIALISATION'),invariant(inv4)],true),po(train_1,'Invariant  establishment',[event('INITIALISATION'),event('INITIALISATION'),invariant(inv5)],true),po(train_1,'Invariant  establishment',[event('INITIALISATION'),event('INITIALISATION'),invariant(inv6)],true),po(train_1,'Invariant  establishment',[event('INITIALISATION'),event('INITIALISATION'),invariant(inv7)],true),po(train_1,'Invariant  establishment',[event('INITIALISATION'),event('INITIALISATION'),invariant(inv8)],true),po(train_1,'Invariant  preservation',[event(route_reservation),event(route_reservation),invariant(inv2)],true),po(train_1,'Invariant  preservation',[event(route_reservation),event(route_reservation),invariant(inv3)],true),po(train_1,'Invariant  preservation',[event(route_reservation),event(route_reservation),invariant(inv4)],true),po(train_1,'Invariant  preservation',[event(route_reservation),event(route_reservation),invariant(inv6)],true),po(train_1,'Invariant  preservation',[event(route_reservation),event(route_reservation),invariant(inv8)],false),po(train_1,'Invariant  preservation',[event(route_freeing),event(route_freeing),invariant(inv2)],true),po(train_1,'Invariant  preservation',[event(route_freeing),event(route_freeing),invariant(inv3)],true),po(train_1,'Invariant  preservation',[event(route_freeing),event(route_freeing),invariant(inv4)],true),po(train_1,'Invariant  preservation',[event(route_freeing),event(route_freeing),invariant(inv6)],true),po(train_1,'Well-definedness of Guard',[guard(grd2),event('FRONT_MOVE_1')],true),po(train_1,'Well-definedness of Guard',[guard(grd3),event('FRONT_MOVE_1')],true),po(train_1,'Invariant  preservation',[event('FRONT_MOVE_1'),event('FRONT_MOVE_1'),invariant(inv3)],false),po(train_1,'Invariant  preservation',[event('FRONT_MOVE_1'),event('FRONT_MOVE_1'),invariant(inv7)],true),po(train_1,'Invariant  preservation',[event('FRONT_MOVE_1'),event('FRONT_MOVE_1'),invariant(inv8)],false),po(train_1,'Guard strengthening (split)',[event('FRONT_MOVE_1'),guard(grd1),event('FRONT_MOVE_1'),event('FRONT_MOVE_1')],true),po(train_1,'Well-definedness of action',[action(act2)],true),po(train_1,'Well-definedness of Guard',[guard(grd3),event('FRONT_MOVE_2')],true),po(train_1,'Well-definedness of witness',[witness(c)],true),po(train_1,'Invariant  preservation',[event('FRONT_MOVE_2'),event('FRONT_MOVE_2'),invariant(inv3)],false),po(train_1,'Invariant  preservation',[event('FRONT_MOVE_2'),event('FRONT_MOVE_2'),invariant(inv7)],true),po(train_1,'Guard strengthening (split)',[event('FRONT_MOVE_2'),guard(grd2),event('FRONT_MOVE_2'),event('FRONT_MOVE_2')],true),po(train_1,'Guard strengthening (split)',[event('FRONT_MOVE_2'),guard(grd3),event('FRONT_MOVE_2'),event('FRONT_MOVE_2')],true),po(train_1,'Well-definedness of action',[action(act1)],true),po(train_1,'Action simulation',[event('FRONT_MOVE_2'),action(act1),event('FRONT_MOVE_2')],true),po(train_1,'Well-definedness of witness',[witness(n)],true),po(train_1,'Invariant  preservation',[event('BACK_MOVE'),event('BACK_MOVE_1'),invariant(inv3)],true),po(train_1,'Invariant  preservation',[event('BACK_MOVE'),event('BACK_MOVE_1'),invariant(inv4)],false),po(train_1,'Invariant  preservation',[event('BACK_MOVE'),event('BACK_MOVE_1'),invariant(inv6)],true),po(train_1,'Invariant  preservation',[event('BACK_MOVE'),event('BACK_MOVE_1'),invariant(inv7)],true),po(train_1,'Invariant  preservation',[event('BACK_MOVE'),event('BACK_MOVE_1'),invariant(inv8)],true),po(train_1,'Guard strengthening (split)',[event('BACK_MOVE'),guard(grd1),event('BACK_MOVE'),event('BACK_MOVE_1')],true),po(train_1,'Guard strengthening (split)',[event('BACK_MOVE'),guard(grd2),event('BACK_MOVE'),event('BACK_MOVE_1')],true),po(train_1,'Guard strengthening (split)',[event('BACK_MOVE'),guard(grd3),event('BACK_MOVE'),event('BACK_MOVE_1')],true),po(train_1,'Guard strengthening (split)',[event('BACK_MOVE'),guard(grd4),event('BACK_MOVE'),event('BACK_MOVE_1')],true),po(train_1,'Well-definedness of Guard',[guard(grd3),event('BACK_MOVE_2')],true),po(train_1,'Well-definedness of witness',[witness(n)],true),po(train_1,'Invariant  preservation',[event('BACK_MOVE'),event('BACK_MOVE_2'),invariant(inv3)],true),po(train_1,'Invariant  preservation',[event('BACK_MOVE'),event('BACK_MOVE_2'),invariant(inv4)],true),po(train_1,'Invariant  preservation',[event('BACK_MOVE'),event('BACK_MOVE_2'),invariant(inv6)],true),po(train_1,'Invariant  preservation',[event('BACK_MOVE'),event('BACK_MOVE_2'),invariant(inv7)],false),po(train_1,'Invariant  preservation',[event('BACK_MOVE'),event('BACK_MOVE_2'),invariant(inv8)],false),po(train_1,'Guard strengthening (split)',[event('BACK_MOVE'),guard(grd1),event('BACK_MOVE'),event('BACK_MOVE_2')],true),po(train_1,'Guard strengthening (split)',[event('BACK_MOVE'),guard(grd2),event('BACK_MOVE'),event('BACK_MOVE_2')],true),po(train_1,'Guard strengthening (split)',[event('BACK_MOVE'),guard(grd3),event('BACK_MOVE'),event('BACK_MOVE_2')],true),po(train_1,'Guard strengthening (split)',[event('BACK_MOVE'),guard(grd4),event('BACK_MOVE'),event('BACK_MOVE_2')],false),po(train_1,'Well-definedness of action',[action(act4)],true),po(train_1,'Invariant  preservation',[event(point_positionning),invariant(inv1)],true),po(train_1,'Invariant  preservation',[event(point_positionning),invariant(inv5)],true),po(train_1,'Invariant  preservation',[event(point_positionning),invariant(inv6)],true),po(train_1,'Well-definedness of action',[action(act1)],true),po(train_1,'Well-definedness of Guard',[guard(grd2),event(route_formation)],true),po(train_1,'Invariant  preservation',[event(route_formation),invariant(inv2)],true),po(train_1,'Invariant  preservation',[event(route_formation),invariant(inv3)],true),po(train_1,'Invariant  preservation',[event(route_formation),invariant(inv4)],true),po(train_1,'Invariant  preservation',[event(route_formation),invariant(inv6)],true),po(train_0,'Well-definedness of Invariant',[invariant(inv6)],true),po(train_0,'Well-definedness of Invariant',[invariant(inv7)],true),po(train_0,'Well-definedness of Invariant',[invariant(inv8)],true),po(train_0,'Invariant  establishment',[event('INITIALISATION'),invariant(inv3)],true),po(train_0,'Invariant  establishment',[event('INITIALISATION'),invariant(inv5)],true),po(train_0,'Invariant  establishment',[event('INITIALISATION'),invariant(inv4)],true),po(train_0,'Invariant  establishment',[event('INITIALISATION'),invariant(inv6)],true),po(train_0,'Invariant  establishment',[event('INITIALISATION'),invariant(inv7)],true),po(train_0,'Invariant  establishment',[event('INITIALISATION'),invariant(inv8)],true),po(train_0,'Invariant  preservation',[event(route_reservation),invariant(inv3)],true),po(train_0,'Invariant  preservation',[event(route_reservation),invariant(inv5)],true),po(train_0,'Invariant  preservation',[event(route_reservation),invariant(inv4)],true),po(train_0,'Invariant  preservation',[event(route_reservation),invariant(inv6)],true),po(train_0,'Invariant  preservation',[event(route_reservation),invariant(inv7)],false),po(train_0,'Invariant  preservation',[event(route_reservation),invariant(inv8)],false),po(train_0,'Invariant  preservation',[event(route_freeing),invariant(inv3)],true),po(train_0,'Well-definedness of Guard',[guard(grd2),event('FRONT_MOVE_1')],true),po(train_0,'Well-definedness of Guard',[guard(grd3),event('FRONT_MOVE_1')],true),po(train_0,'Invariant  preservation',[event('FRONT_MOVE_1'),invariant(inv4)],true),po(train_0,'Invariant  preservation',[event('FRONT_MOVE_1'),invariant(inv6)],true),po(train_0,'Invariant  preservation',[event('FRONT_MOVE_1'),invariant(inv8)],false),po(train_0,'Well-definedness of action',[action(act1)],true),po(train_0,'Well-definedness of Guard',[guard(grd3),event('FRONT_MOVE_2')],true),po(train_0,'Invariant  preservation',[event('FRONT_MOVE_2'),invariant(inv4)],false),po(train_0,'Invariant  preservation',[event('FRONT_MOVE_2'),invariant(inv6)],true),po(train_0,'Invariant  preservation',[event('FRONT_MOVE_2'),invariant(inv8)],false),po(train_0,'Well-definedness of Guard',[guard(grd2),event('BACK_MOVE')],true),po(train_0,'Well-definedness of Guard',[guard(grd3),event('BACK_MOVE')],true),po(train_0,'Well-definedness of Guard',[guard(grd4),event('BACK_MOVE')],true),po(train_0,'Invariant  preservation',[event('BACK_MOVE'),invariant(inv3)],true),po(train_0,'Invariant  preservation',[event('BACK_MOVE'),invariant(inv5)],true),po(train_0,'Invariant  preservation',[event('BACK_MOVE'),invariant(inv4)],true),po(train_0,'Invariant  preservation',[event('BACK_MOVE'),invariant(inv6)],false),po(train_0,'Invariant  preservation',[event('BACK_MOVE'),invariant(inv7)],false),po(train_0,'Invariant  preservation',[event('BACK_MOVE'),invariant(inv8)],true)],_Error)).
+