1

package(load_event_b_project([event_b_model(none,train_4,[sees(none,[train_ctx0,train_ctx1,train_ctx2]),refines(none,train_3),variables(none,[identifier(none,'GRN'),identifier(none,'LBT'),identifier(none,'OCC'),identifier(none,'TRK'),identifier(none,frm),identifier(none,resbl),identifier(none,resrt),identifier(none,rsrtbl)]),invariant(none,[]),theorems(none,[member(rodinpos(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')))]),events(none,[event(rodinpos('INITIALISATION',internal_evt1),'INITIALISATION',ordinary(none),['INITIALISATION'],[],[],[assign(rodinpos(act1,internal_act1),[identifier(none,resrt)],[empty_set(none)]),assign(rodinpos(act2,internal_act2),[identifier(none,resbl)],[empty_set(none)]),assign(rodinpos(act3,internal_act3),[identifier(none,rsrtbl)],[empty_set(none)]),assign(rodinpos(act4,internal_act4),[identifier(none,'OCC')],[empty_set(none)]),assign(rodinpos(act5,internal_element1),[identifier(none,'TRK')],[empty_set(none)]),assign(rodinpos(act6,internal_element2),[identifier(none,frm)],[empty_set(none)]),assign(rodinpos(act7,internal_element3),[identifier(none,'LBT')],[empty_set(none)]),assign(rodinpos(act8,internal_element4),[identifier(none,'GRN')],[empty_set(none)])],[]),event(rodinpos(route_reservation,internal_element1),route_reservation,ordinary(none),[route_reservation],[identifier(rodinpos([],internal_element1),r)],[not_member(rodinpos(grd1,internal_element1),identifier(none,r),identifier(none,resrt)),equal(rodinpos(grd2,internal_element2),intersection(none,image(none,reverse(none,identifier(none,rtbl)),set_extension(none,[identifier(none,r)])),identifier(none,resbl)),empty_set(none))],[assign(rodinpos(act1,internal_element1),[identifier(none,resrt)],[union(none,identifier(none,resrt),set_extension(none,[identifier(none,r)]))]),assign(rodinpos(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(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(route_freeing,internal_element2),route_freeing,ordinary(none),[route_freeing],[identifier(rodinpos([],internal_element1),r)],[member(rodinpos(grd1,internal_element1),identifier(none,r),set_subtraction(none,identifier(none,resrt),range(none,identifier(none,rsrtbl))))],[assign(rodinpos(act1,internal_element1),[identifier(none,resrt)],[set_subtraction(none,identifier(none,resrt),set_extension(none,[identifier(none,r)]))]),assign(rodinpos(act2,internal_element2),[identifier(none,frm)],[set_subtraction(none,identifier(none,frm),set_extension(none,[identifier(none,r)]))])],[]),event(rodinpos('FRONT_MOVE_1',internal_element3),'FRONT_MOVE_1',ordinary(none),['FRONT_MOVE_1'],[identifier(rodinpos([],internal_element1),b)],[member(rodinpos(grd1,internal_element1),identifier(none,b),domain(none,identifier(none,'SIG'))),member(rodinpos(grd2,internal_element2),function(none,identifier(none,'SIG'),[identifier(none,b)]),identifier(none,'GRN'))],[assign(rodinpos(act1,internal_element1),[identifier(none,'OCC')],[union(none,identifier(none,'OCC'),set_extension(none,[identifier(none,b)]))]),assign(rodinpos(act2,internal_element2),[identifier(none,'LBT')],[union(none,identifier(none,'LBT'),set_extension(none,[identifier(none,b)]))]),assign(rodinpos(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('FRONT_MOVE_2',internal_element4),'FRONT_MOVE_2',ordinary(none),['FRONT_MOVE_2'],[identifier(rodinpos([],internal_element1),b)],[member(rodinpos(grd1,internal_element1),identifier(none,b),identifier(none,'OCC')),member(rodinpos(grd2,internal_element2),identifier(none,b),domain(none,identifier(none,'TRK'))),not_member(rodinpos(grd3,internal_element3),function(none,identifier(none,'TRK'),[identifier(none,b)]),identifier(none,'OCC'))],[assign(rodinpos(act1,internal_element1),[identifier(none,'OCC')],[union(none,identifier(none,'OCC'),set_extension(none,[function(none,identifier(none,'TRK'),[identifier(none,b)])]))])],[]),event(rodinpos('BACK_MOVE_1',internal_element5),'BACK_MOVE_1',ordinary(none),['BACK_MOVE_1'],[identifier(rodinpos([],internal_element1),b)],[member(rodinpos(grd1,internal_element1),identifier(none,b),identifier(none,'LBT')),not_member(rodinpos(grd2,internal_element2),identifier(none,b),domain(none,identifier(none,'TRK')))],[assign(rodinpos(act1,internal_element1),[identifier(none,'OCC')],[set_subtraction(none,identifier(none,'OCC'),set_extension(none,[identifier(none,b)]))]),assign(rodinpos(act2,internal_element2),[identifier(none,rsrtbl)],[domain_subtraction(none,set_extension(none,[identifier(none,b)]),identifier(none,rsrtbl))]),assign(rodinpos(act3,internal_element3),[identifier(none,resbl)],[set_subtraction(none,identifier(none,resbl),set_extension(none,[identifier(none,b)]))]),assign(rodinpos(act4,internal_element4),[identifier(none,'LBT')],[set_subtraction(none,identifier(none,'LBT'),set_extension(none,[identifier(none,b)]))])],[]),event(rodinpos('BACK_MOVE_2',internal_element6),'BACK_MOVE_2',ordinary(none),['BACK_MOVE_2'],[identifier(rodinpos([],internal_element1),b)],[member(rodinpos(grd1,internal_element1),identifier(none,b),identifier(none,'LBT')),member(rodinpos(grd2,internal_element2),identifier(none,b),domain(none,identifier(none,'TRK'))),member(rodinpos(grd3,internal_element3),function(none,identifier(none,'TRK'),[identifier(none,b)]),identifier(none,'OCC'))],[assign(rodinpos(act1,internal_element1),[identifier(none,'OCC')],[set_subtraction(none,identifier(none,'OCC'),set_extension(none,[identifier(none,b)]))]),assign(rodinpos(act2,internal_element2),[identifier(none,rsrtbl)],[domain_subtraction(none,set_extension(none,[identifier(none,b)]),identifier(none,rsrtbl))]),assign(rodinpos(act3,internal_element3),[identifier(none,resbl)],[set_subtraction(none,identifier(none,resbl),set_extension(none,[identifier(none,b)]))]),assign(rodinpos(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(point_positionning,internal_element7),point_positionning,ordinary(none),[point_positionning],[identifier(rodinpos([],internal_element1),r)],[member(rodinpos(grd1,internal_element1),identifier(none,r),set_subtraction(none,identifier(none,resrt),identifier(none,frm)))],[assign(rodinpos(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(route_formation,internal_refinesMachine2),route_formation,ordinary(none),[route_formation],[identifier(rodinpos([],'\''),r)],[member(rodinpos(grd1,'('),identifier(none,r),set_subtraction(none,identifier(none,resrt),identifier(none,frm))),equal(rodinpos(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(act1,'*'),[identifier(none,frm)],[union(none,identifier(none,frm),set_extension(none,[identifier(none,r)]))]),assign(rodinpos(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,'GRN'),identifier(none,'LBT'),identifier(none,'OCC'),identifier(none,'TRK'),identifier(none,frm),identifier(none,resbl),identifier(none,resrt),identifier(none,rsrtbl)]),invariant(none,[]),theorems(none,[subset(rodinpos(inv1,internal_element1I),identifier(none,'GRN'),identifier(none,'S')),equal(rodinpos(inv2,internal_element2I),image(none,identifier(none,'SIG'),image(none,identifier(none,fst),identifier(none,rdy))),identifier(none,'GRN')),member(rodinpos(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('INITIALISATION',internal_evt1),'INITIALISATION',ordinary(none),['INITIALISATION'],[],[],[assign(rodinpos(act1,internal_act1),[identifier(none,resrt)],[empty_set(none)]),assign(rodinpos(act2,internal_act2),[identifier(none,resbl)],[empty_set(none)]),assign(rodinpos(act3,internal_act3),[identifier(none,rsrtbl)],[empty_set(none)]),assign(rodinpos(act4,internal_act4),[identifier(none,'OCC')],[empty_set(none)]),assign(rodinpos(act5,internal_element1),[identifier(none,'TRK')],[empty_set(none)]),assign(rodinpos(act6,internal_element2),[identifier(none,frm)],[empty_set(none)]),assign(rodinpos(act7,internal_element3),[identifier(none,'LBT')],[empty_set(none)]),assign(rodinpos(act8,internal_element4),[identifier(none,'GRN')],[empty_set(none)])],[]),event(rodinpos(route_reservation,internal_element1),route_reservation,ordinary(none),[route_reservation],[identifier(rodinpos([],internal_element1),r)],[not_member(rodinpos(grd1,internal_element1),identifier(none,r),identifier(none,resrt)),equal(rodinpos(grd2,internal_element2),intersection(none,image(none,reverse(none,identifier(none,rtbl)),set_extension(none,[identifier(none,r)])),identifier(none,resbl)),empty_set(none))],[assign(rodinpos(act1,internal_element1),[identifier(none,resrt)],[union(none,identifier(none,resrt),set_extension(none,[identifier(none,r)]))]),assign(rodinpos(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(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(route_freeing,internal_element2),route_freeing,ordinary(none),[route_freeing],[identifier(rodinpos([],internal_element1),r)],[member(rodinpos(grd1,internal_element1),identifier(none,r),set_subtraction(none,identifier(none,resrt),range(none,identifier(none,rsrtbl))))],[assign(rodinpos(act1,internal_element1),[identifier(none,resrt)],[set_subtraction(none,identifier(none,resrt),set_extension(none,[identifier(none,r)]))]),assign(rodinpos(act2,internal_element2),[identifier(none,frm)],[set_subtraction(none,identifier(none,frm),set_extension(none,[identifier(none,r)]))])],[]),event(rodinpos('FRONT_MOVE_1',internal_element3),'FRONT_MOVE_1',ordinary(none),['FRONT_MOVE_1'],[identifier(rodinpos([],internal_element1),b)],[member(rodinpos(grd1,internal_element1),identifier(none,b),domain(none,identifier(none,'SIG'))),member(rodinpos(grd2,internal_element2),function(none,identifier(none,'SIG'),[identifier(none,b)]),identifier(none,'GRN'))],[assign(rodinpos(act1,internal_element1),[identifier(none,'OCC')],[union(none,identifier(none,'OCC'),set_extension(none,[identifier(none,b)]))]),assign(rodinpos(act2,internal_element2),[identifier(none,'LBT')],[union(none,identifier(none,'LBT'),set_extension(none,[identifier(none,b)]))]),assign(rodinpos(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(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('FRONT_MOVE_2',internal_element4),'FRONT_MOVE_2',ordinary(none),['FRONT_MOVE_2'],[identifier(rodinpos([],internal_element1),b)],[member(rodinpos(grd1,internal_element1),identifier(none,b),identifier(none,'OCC')),member(rodinpos(grd2,internal_element2),identifier(none,b),domain(none,identifier(none,'TRK'))),not_member(rodinpos(grd3,internal_element3),function(none,identifier(none,'TRK'),[identifier(none,b)]),identifier(none,'OCC'))],[assign(rodinpos(act1,internal_element1),[identifier(none,'OCC')],[union(none,identifier(none,'OCC'),set_extension(none,[function(none,identifier(none,'TRK'),[identifier(none,b)])]))])],[]),event(rodinpos('BACK_MOVE_1',internal_element5),'BACK_MOVE_1',ordinary(none),['BACK_MOVE_1'],[identifier(rodinpos([],internal_element1),b)],[member(rodinpos(grd1,internal_element1),identifier(none,b),identifier(none,'LBT')),not_member(rodinpos(grd2,internal_element2),identifier(none,b),domain(none,identifier(none,'TRK')))],[assign(rodinpos(act1,internal_element1),[identifier(none,'OCC')],[set_subtraction(none,identifier(none,'OCC'),set_extension(none,[identifier(none,b)]))]),assign(rodinpos(act2,internal_element2),[identifier(none,rsrtbl)],[domain_subtraction(none,set_extension(none,[identifier(none,b)]),identifier(none,rsrtbl))]),assign(rodinpos(act3,internal_element3),[identifier(none,resbl)],[set_subtraction(none,identifier(none,resbl),set_extension(none,[identifier(none,b)]))]),assign(rodinpos(act4,internal_element4),[identifier(none,'LBT')],[set_subtraction(none,identifier(none,'LBT'),set_extension(none,[identifier(none,b)]))])],[]),event(rodinpos('BACK_MOVE_2',internal_element6),'BACK_MOVE_2',ordinary(none),['BACK_MOVE_2'],[identifier(rodinpos([],internal_element1),b)],[member(rodinpos(grd1,internal_element1),identifier(none,b),identifier(none,'LBT')),member(rodinpos(grd2,internal_element2),identifier(none,b),domain(none,identifier(none,'TRK'))),member(rodinpos(grd3,internal_element3),function(none,identifier(none,'TRK'),[identifier(none,b)]),identifier(none,'OCC'))],[assign(rodinpos(act1,internal_element1),[identifier(none,'OCC')],[set_subtraction(none,identifier(none,'OCC'),set_extension(none,[identifier(none,b)]))]),assign(rodinpos(act2,internal_element2),[identifier(none,rsrtbl)],[domain_subtraction(none,set_extension(none,[identifier(none,b)]),identifier(none,rsrtbl))]),assign(rodinpos(act3,internal_element3),[identifier(none,resbl)],[set_subtraction(none,identifier(none,resbl),set_extension(none,[identifier(none,b)]))]),assign(rodinpos(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(point_positionning,internal_element7),point_positionning,ordinary(none),[point_positionning],[identifier(rodinpos([],internal_element1),r)],[member(rodinpos(grd1,internal_element1),identifier(none,r),set_subtraction(none,identifier(none,resrt),identifier(none,frm)))],[assign(rodinpos(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(route_formation,internal_refinesMachine2),route_formation,ordinary(none),[route_formation],[identifier(rodinpos([],'\''),r)],[member(rodinpos(grd1,'('),identifier(none,r),set_subtraction(none,identifier(none,resrt),identifier(none,frm))),equal(rodinpos(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(act1,'*'),[identifier(none,frm)],[union(none,identifier(none,frm),set_extension(none,[identifier(none,r)]))]),assign(rodinpos(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,'LBT'),identifier(none,'OCC'),identifier(none,'TRK'),identifier(none,frm),identifier(none,rdy),identifier(none,resbl),identifier(none,resrt),identifier(none,rsrtbl)]),invariant(none,[]),theorems(none,[subset(rodinpos(inv4,internal_refinesMachine3),identifier(none,rdy),identifier(none,frm)),forall(rodinpos(inv2,internal_element2I),[identifier(none,r)],implication(none,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(inv3,internal_element3I),[identifier(none,r)],implication(none,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')),empty_set(none))))]),events(none,[event(rodinpos('INITIALISATION',internal_evt1),'INITIALISATION',ordinary(none),['INITIALISATION'],[],[],[assign(rodinpos(act1,internal_act1),[identifier(none,resrt)],[empty_set(none)]),assign(rodinpos(act2,internal_act2),[identifier(none,resbl)],[empty_set(none)]),assign(rodinpos(act3,internal_act3),[identifier(none,rsrtbl)],[empty_set(none)]),assign(rodinpos(act4,internal_act4),[identifier(none,'OCC')],[empty_set(none)]),assign(rodinpos(act5,internal_element1),[identifier(none,'TRK')],[empty_set(none)]),assign(rodinpos(act6,internal_element2),[identifier(none,frm)],[empty_set(none)]),assign(rodinpos(act7,internal_element3),[identifier(none,'LBT')],[empty_set(none)]),assign(rodinpos(act8,internal_element4),[identifier(none,rdy)],[empty_set(none)])],[]),event(rodinpos(route_reservation,internal_element1),route_reservation,ordinary(none),[route_reservation],[identifier(rodinpos([],internal_element1),r)],[not_member(rodinpos(grd1,internal_element1),identifier(none,r),identifier(none,resrt)),equal(rodinpos(grd2,internal_element2),intersection(none,image(none,reverse(none,identifier(none,rtbl)),set_extension(none,[identifier(none,r)])),identifier(none,resbl)),empty_set(none))],[assign(rodinpos(act1,internal_element1),[identifier(none,resrt)],[union(none,identifier(none,resrt),set_extension(none,[identifier(none,r)]))]),assign(rodinpos(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(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(route_freeing,internal_element2),route_freeing,ordinary(none),[route_freeing],[identifier(rodinpos([],internal_element1),r)],[member(rodinpos(grd1,internal_element1),identifier(none,r),set_subtraction(none,identifier(none,resrt),range(none,identifier(none,rsrtbl))))],[assign(rodinpos(act1,internal_element1),[identifier(none,resrt)],[set_subtraction(none,identifier(none,resrt),set_extension(none,[identifier(none,r)]))]),assign(rodinpos(act2,internal_element2),[identifier(none,frm)],[set_subtraction(none,identifier(none,frm),set_extension(none,[identifier(none,r)]))])],[]),event(rodinpos('FRONT_MOVE_1',internal_element3),'FRONT_MOVE_1',ordinary(none),['FRONT_MOVE_1'],[identifier(rodinpos([],internal_element1),r)],[member(rodinpos(grd1,internal_element1),identifier(none,r),identifier(none,rdy)),equal(rodinpos(grd2,internal_element2),function(none,identifier(none,rsrtbl),[function(none,identifier(none,fst),[identifier(none,r)])]),identifier(none,r))],[assign(rodinpos(act1,internal_element1),[identifier(none,'OCC')],[union(none,identifier(none,'OCC'),set_extension(none,[function(none,identifier(none,fst),[identifier(none,r)])]))]),assign(rodinpos(act2,internal_element2),[identifier(none,'LBT')],[union(none,identifier(none,'LBT'),set_extension(none,[function(none,identifier(none,fst),[identifier(none,r)])]))]),assign(rodinpos(act3,internal_element3),[identifier(none,rdy)],[set_subtraction(none,identifier(none,rdy),set_extension(none,[identifier(none,r)]))])],[]),event(rodinpos('FRONT_MOVE_2',internal_element4),'FRONT_MOVE_2',ordinary(none),['FRONT_MOVE_2'],[identifier(rodinpos([],internal_element1),b)],[member(rodinpos(grd1,internal_element1),identifier(none,b),identifier(none,'OCC')),member(rodinpos(grd2,internal_element2),identifier(none,b),domain(none,identifier(none,'TRK'))),not_member(rodinpos(grd3,internal_element3),function(none,identifier(none,'TRK'),[identifier(none,b)]),identifier(none,'OCC'))],[assign(rodinpos(act1,internal_element1),[identifier(none,'OCC')],[union(none,identifier(none,'OCC'),set_extension(none,[function(none,identifier(none,'TRK'),[identifier(none,b)])]))])],[]),event(rodinpos('BACK_MOVE_1',internal_element5),'BACK_MOVE_1',ordinary(none),['BACK_MOVE_1'],[identifier(rodinpos([],internal_element1),b)],[member(rodinpos(grd1,internal_element1),identifier(none,b),identifier(none,'LBT')),not_member(rodinpos(grd2,internal_element2),identifier(none,b),domain(none,identifier(none,'TRK')))],[assign(rodinpos(act1,internal_element1),[identifier(none,'OCC')],[set_subtraction(none,identifier(none,'OCC'),set_extension(none,[identifier(none,b)]))]),assign(rodinpos(act2,internal_element2),[identifier(none,rsrtbl)],[domain_subtraction(none,set_extension(none,[identifier(none,b)]),identifier(none,rsrtbl))]),assign(rodinpos(act3,internal_element3),[identifier(none,resbl)],[set_subtraction(none,identifier(none,resbl),set_extension(none,[identifier(none,b)]))]),assign(rodinpos(act4,internal_element4),[identifier(none,'LBT')],[set_subtraction(none,identifier(none,'LBT'),set_extension(none,[identifier(none,b)]))])],[]),event(rodinpos('BACK_MOVE_2',internal_element6),'BACK_MOVE_2',ordinary(none),['BACK_MOVE_2'],[identifier(rodinpos([],internal_element1),b)],[member(rodinpos(grd1,internal_element1),identifier(none,b),identifier(none,'LBT')),member(rodinpos(grd2,internal_element2),identifier(none,b),domain(none,identifier(none,'TRK'))),member(rodinpos(grd3,internal_element3),function(none,identifier(none,'TRK'),[identifier(none,b)]),identifier(none,'OCC'))],[assign(rodinpos(act1,internal_element1),[identifier(none,'OCC')],[set_subtraction(none,identifier(none,'OCC'),set_extension(none,[identifier(none,b)]))]),assign(rodinpos(act2,internal_element2),[identifier(none,rsrtbl)],[domain_subtraction(none,set_extension(none,[identifier(none,b)]),identifier(none,rsrtbl))]),assign(rodinpos(act3,internal_element3),[identifier(none,resbl)],[set_subtraction(none,identifier(none,resbl),set_extension(none,[identifier(none,b)]))]),assign(rodinpos(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(point_positionning,internal_evt2),point_positionning,ordinary(none),[point_positionning],[identifier(rodinpos([],internal_var1),r)],[member(rodinpos(grd1,internal_grd1),identifier(none,r),set_subtraction(none,identifier(none,resrt),identifier(none,frm)))],[assign(rodinpos(act1,internal_act1),[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(route_formation,internal_refinesMachine2),route_formation,ordinary(none),[route_formation],[identifier(rodinpos([],'\''),r)],[member(rodinpos(grd1,'('),identifier(none,r),set_subtraction(none,identifier(none,resrt),identifier(none,frm))),equal(rodinpos(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(act2,'+'),[identifier(none,frm)],[union(none,identifier(none,frm),set_extension(none,[identifier(none,r)]))]),assign(rodinpos(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,'LBT'),identifier(none,'OCC'),identifier(none,'TRK'),identifier(none,frm),identifier(none,resbl),identifier(none,resrt),identifier(none,rsrtbl)]),invariant(none,[forall(rodinpos(inv8,internal_element8I),[identifier(none,a),identifier(none,b)],implication(none,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,[member(rodinpos(inv1,internal_element1I),identifier(none,'TRK'),partial_injection(none,identifier(none,'BLOCKS'),identifier(none,'BLOCKS'))),subset(rodinpos(inv2,internal_element2I),identifier(none,frm),identifier(none,resrt)),subset(rodinpos(inv3,internal_element3I),image(none,identifier(none,rsrtbl),identifier(none,'OCC')),identifier(none,frm)),forall(rodinpos(inv4,internal_element4I),[identifier(none,r)],implication(none,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(inv5,internal_element5I),[identifier(none,x),identifier(none,y)],implication(none,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')),member(none,couple(none,[identifier(none,x),identifier(none,y)]),function(none,identifier(none,nxt),[identifier(none,r)])))))),forall(rodinpos(inv6,internal_element6I),[identifier(none,r)],implication(none,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(inv7,internal_element7I),identifier(none,'LBT'),identifier(none,'OCC')),forall(rodinpos(thm1,internal_element1T),[identifier(none,b)],implication(none,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(thm2,internal_element8K),intersection(none,range(none,identifier(none,lst)),set_subtraction(none,domain(none,identifier(none,'TRK')),range(none,identifier(none,fst)))),empty_set(none)),equal(rodinpos(thm3,internal_element8L),intersection(none,range(none,identifier(none,fst)),set_subtraction(none,range(none,identifier(none,'TRK')),range(none,identifier(none,lst)))),empty_set(none))]),events(none,[event(rodinpos('INITIALISATION',internal_evt1),'INITIALISATION',ordinary(none),['INITIALISATION'],[],[],[assign(rodinpos(act1,internal_act1),[identifier(none,resrt)],[empty_set(none)]),assign(rodinpos(act2,internal_act2),[identifier(none,resbl)],[empty_set(none)]),assign(rodinpos(act3,internal_act3),[identifier(none,rsrtbl)],[empty_set(none)]),assign(rodinpos(act4,internal_act4),[identifier(none,'OCC')],[empty_set(none)]),assign(rodinpos(act5,internal_element1),[identifier(none,'TRK')],[empty_set(none)]),assign(rodinpos(act6,internal_element2),[identifier(none,frm)],[empty_set(none)]),assign(rodinpos(act7,internal_element3),[identifier(none,'LBT')],[empty_set(none)])],[]),event(rodinpos(route_reservation,internal_element1),route_reservation,ordinary(none),[route_reservation],[identifier(rodinpos([],internal_element1),r)],[not_member(rodinpos(grd1,internal_element1),identifier(none,r),identifier(none,resrt)),equal(rodinpos(grd2,internal_element2),intersection(none,image(none,reverse(none,identifier(none,rtbl)),set_extension(none,[identifier(none,r)])),identifier(none,resbl)),empty_set(none))],[assign(rodinpos(act1,internal_element1),[identifier(none,resrt)],[union(none,identifier(none,resrt),set_extension(none,[identifier(none,r)]))]),assign(rodinpos(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(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(route_freeing,internal_element2),route_freeing,ordinary(none),[route_freeing],[identifier(rodinpos([],internal_element1),r)],[member(rodinpos(grd1,internal_element1),identifier(none,r),set_subtraction(none,identifier(none,resrt),range(none,identifier(none,rsrtbl))))],[assign(rodinpos(act1,internal_element1),[identifier(none,resrt)],[set_subtraction(none,identifier(none,resrt),set_extension(none,[identifier(none,r)]))]),assign(rodinpos(act2,internal_element2),[identifier(none,frm)],[set_subtraction(none,identifier(none,frm),set_extension(none,[identifier(none,r)]))])],[]),event(rodinpos('FRONT_MOVE_1',internal_element3),'FRONT_MOVE_1',ordinary(none),['FRONT_MOVE_1'],[identifier(rodinpos([],internal_element1),r)],[member(rodinpos(grd1,internal_element1),identifier(none,r),identifier(none,frm)),member(rodinpos(grd2,internal_element2),function(none,identifier(none,fst),[identifier(none,r)]),set_subtraction(none,identifier(none,resbl),identifier(none,'OCC'))),equal(rodinpos(grd3,internal_element3),function(none,identifier(none,rsrtbl),[function(none,identifier(none,fst),[identifier(none,r)])]),identifier(none,r))],[assign(rodinpos(act1,internal_element1),[identifier(none,'OCC')],[union(none,identifier(none,'OCC'),set_extension(none,[function(none,identifier(none,fst),[identifier(none,r)])]))]),assign(rodinpos(act2,internal_element2),[identifier(none,'LBT')],[union(none,identifier(none,'LBT'),set_extension(none,[function(none,identifier(none,fst),[identifier(none,r)])]))])],[]),event(rodinpos('FRONT_MOVE_2',internal_element4),'FRONT_MOVE_2',ordinary(none),['FRONT_MOVE_2'],[identifier(rodinpos([],internal_element1),b)],[member(rodinpos(grd1,internal_element1),identifier(none,b),identifier(none,'OCC')),member(rodinpos(grd2,internal_element2),identifier(none,b),domain(none,identifier(none,'TRK'))),not_member(rodinpos(grd3,internal_element3),function(none,identifier(none,'TRK'),[identifier(none,b)]),identifier(none,'OCC'))],[assign(rodinpos(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(c,internal_wit1),identifier(none,c),function(none,identifier(none,'TRK'),[identifier(none,b)])))]),event(rodinpos('BACK_MOVE_1',internal_element5),'BACK_MOVE_1',ordinary(none),['BACK_MOVE'],[identifier(rodinpos([],internal_element1),b)],[member(rodinpos(grd1,internal_element1),identifier(none,b),identifier(none,'LBT')),not_member(rodinpos(grd2,internal_element2),identifier(none,b),domain(none,identifier(none,'TRK')))],[assign(rodinpos(act1,internal_element1),[identifier(none,'OCC')],[set_subtraction(none,identifier(none,'OCC'),set_extension(none,[identifier(none,b)]))]),assign(rodinpos(act2,internal_element2),[identifier(none,rsrtbl)],[domain_subtraction(none,set_extension(none,[identifier(none,b)]),identifier(none,rsrtbl))]),assign(rodinpos(act3,internal_element3),[identifier(none,resbl)],[set_subtraction(none,identifier(none,resbl),set_extension(none,[identifier(none,b)]))]),assign(rodinpos(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(n,internal_wit1),identifier(none,n),function(none,identifier(none,nxt),[function(none,identifier(none,rsrtbl),[identifier(none,b)])])))]),event(rodinpos('BACK_MOVE_2',internal_element6),'BACK_MOVE_2',ordinary(none),['BACK_MOVE'],[identifier(rodinpos([],internal_element1),b)],[member(rodinpos(grd1,internal_element1),identifier(none,b),identifier(none,'LBT')),member(rodinpos(grd2,internal_element2),identifier(none,b),domain(none,identifier(none,'TRK'))),member(rodinpos(grd3,internal_element3),function(none,identifier(none,'TRK'),[identifier(none,b)]),identifier(none,'OCC'))],[assign(rodinpos(act1,internal_element1),[identifier(none,'OCC')],[set_subtraction(none,identifier(none,'OCC'),set_extension(none,[identifier(none,b)]))]),assign(rodinpos(act2,internal_element2),[identifier(none,rsrtbl)],[domain_subtraction(none,set_extension(none,[identifier(none,b)]),identifier(none,rsrtbl))]),assign(rodinpos(act3,internal_element3),[identifier(none,resbl)],[set_subtraction(none,identifier(none,resbl),set_extension(none,[identifier(none,b)]))]),assign(rodinpos(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(n,internal_wit1),identifier(none,n),function(none,identifier(none,nxt),[function(none,identifier(none,rsrtbl),[identifier(none,b)])])))]),event(rodinpos(point_positionning,internal_element7),point_positionning,ordinary(none),[],[identifier(rodinpos([],internal_element1),r)],[member(rodinpos(grd1,internal_element1),identifier(none,r),set_subtraction(none,identifier(none,resrt),identifier(none,frm)))],[assign(rodinpos(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(route_formation,internal_element8J),route_formation,ordinary(none),[],[identifier(rodinpos([],'\''),r)],[member(rodinpos(grd1,'('),identifier(none,r),set_subtraction(none,identifier(none,resrt),identifier(none,frm))),equal(rodinpos(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(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,'OCC'),identifier(none,resbl),identifier(none,resrt),identifier(none,rsrtbl)]),invariant(none,[subset(rodinpos(inv1,internal_inv1I),identifier(none,resrt),identifier(none,'ROUTES')),subset(rodinpos(inv2,internal_inv2I),identifier(none,resbl),identifier(none,'BLOCKS')),member(rodinpos(inv3,internal_inv3I),identifier(none,rsrtbl),total_function(none,identifier(none,resbl),identifier(none,resrt))),subset(rodinpos(inv5,internal_inv5I),identifier(none,rsrtbl),identifier(none,rtbl)),subset(rodinpos(inv4,internal_inv4I),identifier(none,'OCC'),identifier(none,resbl)),forall(rodinpos(inv6,internal_element1I),[identifier(none,r)],implication(none,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'))),empty_set(none)))),forall(rodinpos(inv7,internal_element2I),[identifier(none,r)],implication(none,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(inv8,internal_element3I),[identifier(none,r)],implication(none,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('INITIALISATION',internal_evt1),'INITIALISATION',ordinary(none),[],[],[],[assign(rodinpos(act1,internal_act1),[identifier(none,resrt)],[empty_set(none)]),assign(rodinpos(act2,internal_act2),[identifier(none,resbl)],[empty_set(none)]),assign(rodinpos(act3,internal_act3),[identifier(none,rsrtbl)],[empty_set(none)]),assign(rodinpos(act4,internal_act4),[identifier(none,'OCC')],[empty_set(none)])],[]),event(rodinpos(route_reservation,internal_element1),route_reservation,ordinary(none),[],[identifier(rodinpos([],internal_element1),r)],[not_member(rodinpos(grd1,internal_element1),identifier(none,r),identifier(none,resrt)),equal(rodinpos(grd2,internal_element2),intersection(none,image(none,reverse(none,identifier(none,rtbl)),set_extension(none,[identifier(none,r)])),identifier(none,resbl)),empty_set(none))],[assign(rodinpos(act1,internal_element1),[identifier(none,resrt)],[union(none,identifier(none,resrt),set_extension(none,[identifier(none,r)]))]),assign(rodinpos(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(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(route_freeing,internal_element2),route_freeing,ordinary(none),[],[identifier(rodinpos([],internal_element1),r)],[member(rodinpos(grd1,internal_element1),identifier(none,r),set_subtraction(none,identifier(none,resrt),range(none,identifier(none,rsrtbl))))],[assign(rodinpos(act1,internal_element1),[identifier(none,resrt)],[set_subtraction(none,identifier(none,resrt),set_extension(none,[identifier(none,r)]))])],[]),event(rodinpos('FRONT_MOVE_1',internal_element3),'FRONT_MOVE_1',ordinary(none),[],[identifier(rodinpos([],internal_element1),r)],[member(rodinpos(grd1,internal_element1),identifier(none,r),identifier(none,resrt)),member(rodinpos(grd2,internal_element2),function(none,identifier(none,fst),[identifier(none,r)]),set_subtraction(none,identifier(none,resbl),identifier(none,'OCC'))),equal(rodinpos(grd3,internal_element3),function(none,identifier(none,rsrtbl),[function(none,identifier(none,fst),[identifier(none,r)])]),identifier(none,r))],[assign(rodinpos(act1,internal_element1),[identifier(none,'OCC')],[union(none,identifier(none,'OCC'),set_extension(none,[function(none,identifier(none,fst),[identifier(none,r)])]))])],[]),event(rodinpos('FRONT_MOVE_2',internal_element4),'FRONT_MOVE_2',ordinary(none),[],[identifier(rodinpos([],internal_element1),b),identifier(rodinpos([],internal_element2),c)],[member(rodinpos(grd1,internal_element1),identifier(none,b),identifier(none,'OCC')),not_member(rodinpos(grd2,internal_element2),identifier(none,c),identifier(none,'OCC')),member(rodinpos(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(act1,internal_element1),[identifier(none,'OCC')],[union(none,identifier(none,'OCC'),set_extension(none,[identifier(none,c)]))])],[]),event(rodinpos('BACK_MOVE',internal_element5),'BACK_MOVE',ordinary(none),[],[identifier(rodinpos([],internal_element1),b),identifier(rodinpos([],internal_element2),n)],[member(rodinpos(grd1,internal_element1),identifier(none,b),identifier(none,'OCC')),equal(rodinpos(grd2,internal_element2),identifier(none,n),function(none,identifier(none,nxt),[function(none,identifier(none,rsrtbl),[identifier(none,b)])])),implication(rodinpos(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(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(act1,internal_element1),[identifier(none,'OCC')],[set_subtraction(none,identifier(none,'OCC'),set_extension(none,[identifier(none,b)]))]),assign(rodinpos(act2,internal_element2),[identifier(none,rsrtbl)],[domain_subtraction(none,set_extension(none,[identifier(none,b)]),identifier(none,rsrtbl))]),assign(rodinpos(act3,internal_element3),[identifier(none,resbl)],[set_subtraction(none,identifier(none,resbl),set_extension(none,[identifier(none,b)]))])],[])])])],[event_b_context(none,train_ctx2,[extends(none,[train_ctx1]),constants(none,[identifier(none,blpt),identifier(none,lft),identifier(none,rht)]),axioms(none,[]),theorems(none,[subset(rodinpos(axm1,internal_axm1A),identifier(none,blpt),identifier(none,'BLOCKS')),member(rodinpos(axm2,internal_axm2A),identifier(none,lft),total_function(none,identifier(none,blpt),identifier(none,'BLOCKS'))),member(rodinpos(axm3,internal_axm3A),identifier(none,rht),total_function(none,identifier(none,blpt),identifier(none,'BLOCKS'))),equal(rodinpos(axm4,internal_axm4A),intersection(none,identifier(none,lft),identifier(none,rht)),empty_set(none)),forall(rodinpos(axm5,internal_axm5A),[identifier(none,r)],implication(none,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(axm6,internal_axm6A),intersection(none,identifier(none,blpt),range(none,identifier(none,fst))),empty_set(none)),equal(rodinpos(axm7,internal_axm7A),intersection(none,identifier(none,blpt),range(none,identifier(none,lst))),empty_set(none))]),sets(none,[])]),event_b_context(none,train_ctx1,[extends(none,[train_ctx0]),constants(none,[identifier(none,'S1'),identifier(none,'S2'),identifier(none,'S3'),identifier(none,'S4'),identifier(none,'S5'),identifier(none,'SIG')]),axioms(none,[partition(rodinpos(axm3,internal_extendsContext3),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(axm4,internal_extendsContext9),identifier(none,'SIG'),set_extension(none,[couple(none,[identifier(none,'A'),identifier(none,'S1')]),couple(none,[identifier(none,'H'),identifier(none,'S2')]),couple(none,[identifier(none,'I'),identifier(none,'S3')]),couple(none,[identifier(none,'C'),identifier(none,'S4')]),couple(none,[identifier(none,'F'),identifier(none,'S5')])]))]),theorems(none,[member(rodinpos(axm1,internal_axm1A),identifier(none,'SIG'),total_bijection(none,range(none,identifier(none,fst)),identifier(none,'S'))),equal(rodinpos(axm2,internal_extendsContext2),card(none,identifier(none,'S')),integer(none,5))]),sets(none,[deferred_set(none,'S')])]),event_b_context(none,train_ctx0,[extends(none,[]),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,'R1'),identifier(none,'R2'),identifier(none,'R3'),identifier(none,'R4'),identifier(none,'R5'),identifier(none,'R6'),identifier(none,'R7'),identifier(none,'R8'),identifier(none,fst),identifier(none,lst),identifier(none,nxt),identifier(none,rtbl)]),axioms(none,[partition(rodinpos(axm44,internal_axm144),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')])]),partition(rodinpos(axm45,internal_axm149),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')])]),equal(rodinpos(axm14,internal_axm13B),identifier(none,rtbl),set_extension(none,[couple(none,[identifier(none,'A'),identifier(none,'R1')]),couple(none,[identifier(none,'A'),identifier(none,'R2')]),couple(none,[identifier(none,'A'),identifier(none,'R5')]),couple(none,[identifier(none,'A'),identifier(none,'R6')]),couple(none,[identifier(none,'B'),identifier(none,'R1')]),couple(none,[identifier(none,'B'),identifier(none,'R2')]),couple(none,[identifier(none,'B'),identifier(none,'R5')]),couple(none,[identifier(none,'B'),identifier(none,'R6')]),couple(none,[identifier(none,'C'),identifier(none,'R1')]),couple(none,[identifier(none,'C'),identifier(none,'R5')]),couple(none,[identifier(none,'D'),identifier(none,'R2')]),couple(none,[identifier(none,'D'),identifier(none,'R6')]),couple(none,[identifier(none,'E'),identifier(none,'R2')]),couple(none,[identifier(none,'E'),identifier(none,'R3')]),couple(none,[identifier(none,'E'),identifier(none,'R4')]),couple(none,[identifier(none,'E'),identifier(none,'R6')]),couple(none,[identifier(none,'E'),identifier(none,'R7')]),couple(none,[identifier(none,'E'),identifier(none,'R8')]),couple(none,[identifier(none,'F'),identifier(none,'R2')]),couple(none,[identifier(none,'F'),identifier(none,'R3')]),couple(none,[identifier(none,'F'),identifier(none,'R4')]),couple(none,[identifier(none,'F'),identifier(none,'R6')]),couple(none,[identifier(none,'F'),identifier(none,'R7')]),couple(none,[identifier(none,'F'),identifier(none,'R8')]),couple(none,[identifier(none,'G'),identifier(none,'R3')]),couple(none,[identifier(none,'G'),identifier(none,'R4')]),couple(none,[identifier(none,'G'),identifier(none,'R4')]),couple(none,[identifier(none,'G'),identifier(none,'R7')]),couple(none,[identifier(none,'G'),identifier(none,'R8')]),couple(none,[identifier(none,'H'),identifier(none,'R3')]),couple(none,[identifier(none,'H'),identifier(none,'R7')]),couple(none,[identifier(none,'I'),identifier(none,'R4')]),couple(none,[identifier(none,'I'),identifier(none,'R8')])])),equal(rodinpos(axm40,internal_axm13u),identifier(none,nxt),set_extension(none,[couple(none,[identifier(none,'R1'),set_extension(none,[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,'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,'R3'),set_extension(none,[couple(none,[identifier(none,'H'),identifier(none,'G')]),couple(none,[identifier(none,'G'),identifier(none,'E')]),couple(none,[identifier(none,'E'),identifier(none,'F')])])]),couple(none,[identifier(none,'R4'),set_extension(none,[couple(none,[identifier(none,'I'),identifier(none,'G')]),couple(none,[identifier(none,'G'),identifier(none,'E')]),couple(none,[identifier(none,'E'),identifier(none,'F')])])]),couple(none,[identifier(none,'R5'),set_extension(none,[couple(none,[identifier(none,'C'),identifier(none,'B')]),couple(none,[identifier(none,'B'),identifier(none,'A')])])]),couple(none,[identifier(none,'R6'),set_extension(none,[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,'R7'),set_extension(none,[couple(none,[identifier(none,'F'),identifier(none,'E')]),couple(none,[identifier(none,'E'),identifier(none,'G')]),couple(none,[identifier(none,'G'),identifier(none,'H')])])]),couple(none,[identifier(none,'R8'),set_extension(none,[couple(none,[identifier(none,'F'),identifier(none,'E')]),couple(none,[identifier(none,'E'),identifier(none,'G')]),couple(none,[identifier(none,'G'),identifier(none,'I')])])])])),equal(rodinpos(axm41,internal_axm13v),identifier(none,fst),set_extension(none,[couple(none,[identifier(none,'R1'),identifier(none,'A')]),couple(none,[identifier(none,'R2'),identifier(none,'A')]),couple(none,[identifier(none,'R3'),identifier(none,'H')]),couple(none,[identifier(none,'R4'),identifier(none,'I')]),couple(none,[identifier(none,'R5'),identifier(none,'C')]),couple(none,[identifier(none,'R6'),identifier(none,'F')]),couple(none,[identifier(none,'R7'),identifier(none,'F')]),couple(none,[identifier(none,'R8'),identifier(none,'F')])])),equal(rodinpos(axm42,internal_axm13w),identifier(none,lst),set_extension(none,[couple(none,[identifier(none,'R1'),identifier(none,'C')]),couple(none,[identifier(none,'R2'),identifier(none,'F')]),couple(none,[identifier(none,'R3'),identifier(none,'F')]),couple(none,[identifier(none,'R4'),identifier(none,'F')]),couple(none,[identifier(none,'R5'),identifier(none,'A')]),couple(none,[identifier(none,'R6'),identifier(none,'A')]),couple(none,[identifier(none,'R7'),identifier(none,'H')]),couple(none,[identifier(none,'R8'),identifier(none,'I')])]))]),theorems(none,[member(rodinpos(axm1,internal_axm1A),identifier(none,rtbl),relations(none,identifier(none,'BLOCKS'),identifier(none,'ROUTES'))),equal(rodinpos(axm2,internal_axm2A),domain(none,identifier(none,rtbl)),identifier(none,'BLOCKS')),equal(rodinpos(axm3,internal_axm3A),range(none,identifier(none,rtbl)),identifier(none,'ROUTES')),member(rodinpos(axm4,internal_axm4A),identifier(none,nxt),total_function(none,identifier(none,'ROUTES'),partial_injection(none,identifier(none,'BLOCKS'),identifier(none,'BLOCKS')))),member(rodinpos(axm5,internal_axm5A),identifier(none,fst),total_function(none,identifier(none,'ROUTES'),identifier(none,'BLOCKS'))),member(rodinpos(axm6,internal_axm6A),identifier(none,lst),total_function(none,identifier(none,'ROUTES'),identifier(none,'BLOCKS'))),subset(rodinpos(axm7,internal_axm7A),reverse(none,identifier(none,fst)),identifier(none,rtbl)),subset(rodinpos(axm8,internal_axm8A),reverse(none,identifier(none,lst)),identifier(none,rtbl)),forall(rodinpos(axm11,internal_axm11A),[identifier(none,r)],implication(none,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(axm10,internal_axm10A),[identifier(none,r)],implication(none,member(none,identifier(none,r),identifier(none,'ROUTES')),forall(none,[identifier(none,'S')],implication(none,conjunct(none,subset(none,identifier(none,'S'),identifier(none,'BLOCKS')),subset(none,identifier(none,'S'),image(none,function(none,identifier(none,nxt),[identifier(none,r)]),identifier(none,'S')))),equal(none,identifier(none,'S'),empty_set(none)))))),forall(rodinpos(axm9,internal_axm9A),[identifier(none,r)],implication(none,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(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')),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(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')),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)])])))))]),sets(none,[deferred_set(none,'BLOCKS'),deferred_set(none,'ROUTES')])])],[discharged(train_1,'INITIALISATION',inv8),discharged(train_0,'INITIALISATION',inv5),discharged(train_0,'INITIALISATION',inv4),wp('BACK_MOVE_1','BACK_MOVE_1',[member(none,identifier(none,b),set_subtraction(none,identifier(none,'LBT'),set_extension(none,[identifier(none,b)]))),not_member(none,identifier(none,b),domain(none,identifier(none,'TRK')))]),wp('BACK_MOVE_1','BACK_MOVE_2',[member(none,identifier(none,b),set_subtraction(none,identifier(none,'LBT'),set_extension(none,[identifier(none,b)]))),member(none,identifier(none,b),domain(none,identifier(none,'TRK'))),member(none,function(none,identifier(none,'TRK'),[identifier(none,b)]),set_subtraction(none,identifier(none,'OCC'),set_extension(none,[identifier(none,b)])))]),wp('BACK_MOVE_1','FRONT_MOVE_2',[member(none,identifier(none,b),set_subtraction(none,identifier(none,'OCC'),set_extension(none,[identifier(none,b)]))),member(none,identifier(none,b),domain(none,identifier(none,'TRK'))),not_member(none,function(none,identifier(none,'TRK'),[identifier(none,b)]),set_subtraction(none,identifier(none,'OCC'),set_extension(none,[identifier(none,b)])))]),wp('BACK_MOVE_1',route_formation,[member(none,identifier(none,r),set_subtraction(none,identifier(none,resrt),identifier(none,frm))),equal(none,domain_restriction(none,image(none,reverse(none,domain_subtraction(none,set_extension(none,[identifier(none,b)]),identifier(none,rsrtbl))),set_extension(none,[identifier(none,r)])),function(none,identifier(none,nxt),[identifier(none,r)])),domain_restriction(none,image(none,reverse(none,domain_subtraction(none,set_extension(none,[identifier(none,b)]),identifier(none,rsrtbl))),set_extension(none,[identifier(none,r)])),identifier(none,'TRK')))]),wp('BACK_MOVE_1',route_freeing,[member(none,identifier(none,r),set_subtraction(none,identifier(none,resrt),range(none,domain_subtraction(none,set_extension(none,[identifier(none,b)]),identifier(none,rsrtbl)))))]),wp('BACK_MOVE_1',route_reservation,[not_member(none,identifier(none,r),identifier(none,resrt)),equal(none,intersection(none,image(none,reverse(none,identifier(none,rtbl)),set_extension(none,[identifier(none,r)])),set_subtraction(none,identifier(none,resbl),set_extension(none,[identifier(none,b)]))),empty_set(none))]),wp('BACK_MOVE_2','BACK_MOVE_1',[member(none,identifier(none,b),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)])]))),not_member(none,identifier(none,b),domain(none,identifier(none,'TRK')))]),wp('BACK_MOVE_2','BACK_MOVE_2',[member(none,identifier(none,b),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)])]))),member(none,identifier(none,b),domain(none,identifier(none,'TRK'))),member(none,function(none,identifier(none,'TRK'),[identifier(none,b)]),set_subtraction(none,identifier(none,'OCC'),set_extension(none,[identifier(none,b)])))]),wp('BACK_MOVE_2','FRONT_MOVE_2',[member(none,identifier(none,b),set_subtraction(none,identifier(none,'OCC'),set_extension(none,[identifier(none,b)]))),member(none,identifier(none,b),domain(none,identifier(none,'TRK'))),not_member(none,function(none,identifier(none,'TRK'),[identifier(none,b)]),set_subtraction(none,identifier(none,'OCC'),set_extension(none,[identifier(none,b)])))]),wp('BACK_MOVE_2',route_formation,[member(none,identifier(none,r),set_subtraction(none,identifier(none,resrt),identifier(none,frm))),equal(none,domain_restriction(none,image(none,reverse(none,domain_subtraction(none,set_extension(none,[identifier(none,b)]),identifier(none,rsrtbl))),set_extension(none,[identifier(none,r)])),function(none,identifier(none,nxt),[identifier(none,r)])),domain_restriction(none,image(none,reverse(none,domain_subtraction(none,set_extension(none,[identifier(none,b)]),identifier(none,rsrtbl))),set_extension(none,[identifier(none,r)])),identifier(none,'TRK')))]),wp('BACK_MOVE_2',route_freeing,[member(none,identifier(none,r),set_subtraction(none,identifier(none,resrt),range(none,domain_subtraction(none,set_extension(none,[identifier(none,b)]),identifier(none,rsrtbl)))))]),wp('BACK_MOVE_2',route_reservation,[not_member(none,identifier(none,r),identifier(none,resrt)),equal(none,intersection(none,image(none,reverse(none,identifier(none,rtbl)),set_extension(none,[identifier(none,r)])),set_subtraction(none,identifier(none,resbl),set_extension(none,[identifier(none,b)]))),empty_set(none))]),wp('FRONT_MOVE_1','BACK_MOVE_1',[member(none,identifier(none,b),union(none,identifier(none,'LBT'),set_extension(none,[identifier(none,b)]))),not_member(none,identifier(none,b),domain(none,identifier(none,'TRK')))]),wp('FRONT_MOVE_1','BACK_MOVE_2',[member(none,identifier(none,b),union(none,identifier(none,'LBT'),set_extension(none,[identifier(none,b)]))),member(none,identifier(none,b),domain(none,identifier(none,'TRK'))),member(none,function(none,identifier(none,'TRK'),[identifier(none,b)]),union(none,identifier(none,'OCC'),set_extension(none,[identifier(none,b)])))]),wp('FRONT_MOVE_1','FRONT_MOVE_1',[member(none,identifier(none,b),domain(none,identifier(none,'SIG'))),member(none,function(none,identifier(none,'SIG'),[identifier(none,b)]),set_subtraction(none,identifier(none,'GRN'),set_extension(none,[function(none,identifier(none,'SIG'),[identifier(none,b)])])))]),wp('FRONT_MOVE_1','FRONT_MOVE_2',[member(none,identifier(none,b),union(none,identifier(none,'OCC'),set_extension(none,[identifier(none,b)]))),member(none,identifier(none,b),domain(none,identifier(none,'TRK'))),not_member(none,function(none,identifier(none,'TRK'),[identifier(none,b)]),union(none,identifier(none,'OCC'),set_extension(none,[identifier(none,b)])))]),wp('FRONT_MOVE_2','BACK_MOVE_2',[member(none,identifier(none,b),identifier(none,'LBT')),member(none,identifier(none,b),domain(none,identifier(none,'TRK'))),member(none,function(none,identifier(none,'TRK'),[identifier(none,b)]),union(none,identifier(none,'OCC'),set_extension(none,[function(none,identifier(none,'TRK'),[identifier(none,b)])])))]),wp('FRONT_MOVE_2','FRONT_MOVE_2',[member(none,identifier(none,b),union(none,identifier(none,'OCC'),set_extension(none,[function(none,identifier(none,'TRK'),[identifier(none,b)])]))),member(none,identifier(none,b),domain(none,identifier(none,'TRK'))),not_member(none,function(none,identifier(none,'TRK'),[identifier(none,b)]),union(none,identifier(none,'OCC'),set_extension(none,[function(none,identifier(none,'TRK'),[identifier(none,b)])])))]),wp('INITIALISATION','BACK_MOVE_1',[member(none,identifier(none,b),empty_set(none)),not_member(none,identifier(none,b),domain(none,empty_set(none)))]),wp('INITIALISATION','BACK_MOVE_2',[member(none,identifier(none,b),empty_set(none)),member(none,identifier(none,b),domain(none,empty_set(none))),member(none,function(none,empty_set(none),[identifier(none,b)]),empty_set(none))]),wp('INITIALISATION','FRONT_MOVE_1',[member(none,identifier(none,b),domain(none,identifier(none,'SIG'))),member(none,function(none,identifier(none,'SIG'),[identifier(none,b)]),empty_set(none))]),wp('INITIALISATION','FRONT_MOVE_2',[member(none,identifier(none,b),empty_set(none)),member(none,identifier(none,b),domain(none,empty_set(none))),not_member(none,function(none,empty_set(none),[identifier(none,b)]),empty_set(none))]),wp('INITIALISATION',point_positionning,[member(none,identifier(none,r),set_subtraction(none,empty_set(none),empty_set(none)))]),wp('INITIALISATION',route_formation,[member(none,identifier(none,r),set_subtraction(none,empty_set(none),empty_set(none))),equal(none,domain_restriction(none,image(none,reverse(none,empty_set(none)),set_extension(none,[identifier(none,r)])),function(none,identifier(none,nxt),[identifier(none,r)])),domain_restriction(none,image(none,reverse(none,empty_set(none)),set_extension(none,[identifier(none,r)])),empty_set(none)))]),wp('INITIALISATION',route_freeing,[member(none,identifier(none,r),set_subtraction(none,empty_set(none),range(none,empty_set(none))))]),wp('INITIALISATION',route_reservation,[not_member(none,identifier(none,r),empty_set(none)),equal(none,intersection(none,image(none,reverse(none,identifier(none,rtbl)),set_extension(none,[identifier(none,r)])),empty_set(none)),empty_set(none))]),wp(point_positionning,'BACK_MOVE_1',[member(none,identifier(none,b),identifier(none,'LBT')),not_member(none,identifier(none,b),domain(none,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)]))))]),wp(point_positionning,'BACK_MOVE_2',[member(none,identifier(none,b),identifier(none,'LBT')),member(none,identifier(none,b),domain(none,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)])))),member(none,function(none,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)])),[identifier(none,b)]),identifier(none,'OCC'))]),wp(point_positionning,'FRONT_MOVE_2',[member(none,identifier(none,b),identifier(none,'OCC')),member(none,identifier(none,b),domain(none,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)])))),not_member(none,function(none,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)])),[identifier(none,b)]),identifier(none,'OCC'))]),wp(point_positionning,route_formation,[member(none,identifier(none,r),set_subtraction(none,identifier(none,resrt),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)])),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)]))))]),wp(route_formation,'FRONT_MOVE_1',[member(none,identifier(none,b),domain(none,identifier(none,'SIG'))),member(none,function(none,identifier(none,'SIG'),[identifier(none,b)]),union(none,identifier(none,'GRN'),set_extension(none,[function(none,identifier(none,'SIG'),[function(none,identifier(none,fst),[identifier(none,r)])])])))]),wp(route_formation,point_positionning,[member(none,identifier(none,r),set_subtraction(none,identifier(none,resrt),union(none,identifier(none,frm),set_extension(none,[identifier(none,r)]))))]),wp(route_formation,route_formation,[member(none,identifier(none,r),set_subtraction(none,identifier(none,resrt),union(none,identifier(none,frm),set_extension(none,[identifier(none,r)])))),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')))]),wp(route_freeing,point_positionning,[member(none,identifier(none,r),set_subtraction(none,set_subtraction(none,identifier(none,resrt),set_extension(none,[identifier(none,r)])),set_subtraction(none,identifier(none,frm),set_extension(none,[identifier(none,r)]))))]),wp(route_freeing,route_formation,[member(none,identifier(none,r),set_subtraction(none,set_subtraction(none,identifier(none,resrt),set_extension(none,[identifier(none,r)])),set_subtraction(none,identifier(none,frm),set_extension(none,[identifier(none,r)])))),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')))]),wp(route_freeing,route_freeing,[member(none,identifier(none,r),set_subtraction(none,set_subtraction(none,identifier(none,resrt),set_extension(none,[identifier(none,r)])),range(none,identifier(none,rsrtbl))))]),wp(route_freeing,route_reservation,[not_member(none,identifier(none,r),set_subtraction(none,identifier(none,resrt),set_extension(none,[identifier(none,r)]))),equal(none,intersection(none,image(none,reverse(none,identifier(none,rtbl)),set_extension(none,[identifier(none,r)])),identifier(none,resbl)),empty_set(none))]),wp(route_reservation,point_positionning,[member(none,identifier(none,r),set_subtraction(none,union(none,identifier(none,resrt),set_extension(none,[identifier(none,r)])),identifier(none,frm)))]),wp(route_reservation,route_formation,[member(none,identifier(none,r),set_subtraction(none,union(none,identifier(none,resrt),set_extension(none,[identifier(none,r)])),identifier(none,frm))),equal(none,domain_restriction(none,image(none,reverse(none,union(none,identifier(none,rsrtbl),range_restriction(none,identifier(none,rtbl),set_extension(none,[identifier(none,r)])))),set_extension(none,[identifier(none,r)])),function(none,identifier(none,nxt),[identifier(none,r)])),domain_restriction(none,image(none,reverse(none,union(none,identifier(none,rsrtbl),range_restriction(none,identifier(none,rtbl),set_extension(none,[identifier(none,r)])))),set_extension(none,[identifier(none,r)])),identifier(none,'TRK')))]),wp(route_reservation,route_freeing,[member(none,identifier(none,r),set_subtraction(none,union(none,identifier(none,resrt),set_extension(none,[identifier(none,r)])),range(none,union(none,identifier(none,rsrtbl),range_restriction(none,identifier(none,rtbl),set_extension(none,[identifier(none,r)]))))))]),wp(route_reservation,route_reservation,[not_member(none,identifier(none,r),union(none,identifier(none,resrt),set_extension(none,[identifier(none,r)]))),equal(none,intersection(none,image(none,reverse(none,identifier(none,rtbl)),set_extension(none,[identifier(none,r)])),union(none,identifier(none,resbl),image(none,reverse(none,identifier(none,rtbl)),set_extension(none,[identifier(none,r)])))),empty_set(none))]),nonchanging_guard('INITIALISATION',[]),nonchanging_guard(route_reservation,[]),nonchanging_guard(route_freeing,[]),nonchanging_guard('FRONT_MOVE_1',[member(none,identifier(none,b),domain(none,identifier(none,'SIG')))]),nonchanging_guard('FRONT_MOVE_2',[member(none,identifier(none,b),domain(none,identifier(none,'TRK')))]),nonchanging_guard('BACK_MOVE_1',[not_member(none,identifier(none,b),domain(none,identifier(none,'TRK')))]),nonchanging_guard('BACK_MOVE_2',[member(none,identifier(none,b),domain(none,identifier(none,'TRK')))]),nonchanging_guard(point_positionning,[member(none,identifier(none,r),set_subtraction(none,identifier(none,resrt),identifier(none,frm)))]),nonchanging_guard(route_formation,[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')))])],Error)).