diff --git a/Train_B_Book/train_1_beebook_mch.eventb b/Train_B_Book/train_1_beebook_mch.eventb new file mode 100644 index 0000000000000000000000000000000000000000..23b46ca244da6d374d00b2a8548f98fb185fb3e4 --- /dev/null +++ b/Train_B_Book/train_1_beebook_mch.eventb @@ -0,0 +1,2 @@ +package(load_event_b_project([event_b_model(none,train_1_beebook,[sees(none,[train_ctx0,train_ctx0_beebook]),refines(none,train_1),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,[]),theorems(none,[]),events(none,[event(rodinpos(train_1_beebook,'INITIALISATION',internal_element4),'INITIALISATION',ordinary(none),['INITIALISATION'],[],[],[],[assign(rodinpos(train_1_beebook,act1,internal_act1),[identifier(none,resrt)],[typeof(none,empty_set(none),pow_subset(none,identifier(none,'ROUTES')))]),assign(rodinpos(train_1_beebook,act2,internal_act2),[identifier(none,resbl)],[typeof(none,empty_set(none),pow_subset(none,identifier(none,'BLOCKS')))]),assign(rodinpos(train_1_beebook,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_beebook,act4,internal_act4),[identifier(none,'OCC')],[typeof(none,empty_set(none),pow_subset(none,identifier(none,'BLOCKS')))]),assign(rodinpos(train_1_beebook,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_beebook,act6,internal_element2),[identifier(none,frm)],[typeof(none,empty_set(none),pow_subset(none,identifier(none,'ROUTES')))]),assign(rodinpos(train_1_beebook,act7,internal_element3),[identifier(none,'LBT')],[typeof(none,empty_set(none),pow_subset(none,identifier(none,'BLOCKS')))])],[]),event(rodinpos(train_1_beebook,route_reservation,internal_element5),route_reservation,ordinary(none),[route_reservation],[identifier(rodinpos(train_1_beebook,[],internal_element1),r)],[not_member(rodinpos(train_1_beebook,grd1,internal_element1),identifier(none,r),identifier(none,resrt)),equal(rodinpos(train_1_beebook,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_beebook,act1,internal_element1),[identifier(none,resrt)],[union(none,identifier(none,resrt),set_extension(none,[identifier(none,r)]))]),assign(rodinpos(train_1_beebook,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_beebook,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_beebook,route_freeing,internal_element6),route_freeing,ordinary(none),[route_freeing],[identifier(rodinpos(train_1_beebook,[],internal_element1),r)],[member(rodinpos(train_1_beebook,grd1,internal_element1),identifier(none,r),set_subtraction(none,identifier(none,resrt),range(none,identifier(none,rsrtbl))))],[],[assign(rodinpos(train_1_beebook,act1,internal_element1),[identifier(none,resrt)],[set_subtraction(none,identifier(none,resrt),set_extension(none,[identifier(none,r)]))]),assign(rodinpos(train_1_beebook,act2,internal_element2),[identifier(none,frm)],[set_subtraction(none,identifier(none,frm),set_extension(none,[identifier(none,r)]))])],[]),event(rodinpos(train_1_beebook,'FRONT_MOVE_1',internal_element7),'FRONT_MOVE_1',ordinary(none),['FRONT_MOVE_1'],[identifier(rodinpos(train_1_beebook,[],'_QdStMIdPEeOSfLkA9HaR6w'),r)],[member(rodinpos(train_1_beebook,grd1,'_QdStMYdPEeOSfLkA9HaR6w'),identifier(none,r),identifier(none,frm)),member(rodinpos(train_1_beebook,grd2,'_QdStModPEeOSfLkA9HaR6w'),function(none,identifier(none,fst),[identifier(none,r)]),set_subtraction(none,identifier(none,resbl),identifier(none,'OCC'))),equal(rodinpos(train_1_beebook,grd3,'_QdTUQIdPEeOSfLkA9HaR6w'),function(none,identifier(none,rsrtbl),[function(none,identifier(none,fst),[identifier(none,r)])]),identifier(none,r))],[],[assign(rodinpos(train_1_beebook,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_beebook,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_beebook,'FRONT_MOVE_2',internal_element8),'FRONT_MOVE_2',ordinary(none),['FRONT_MOVE_2'],[identifier(rodinpos(train_1_beebook,[],internal_element1),b)],[member(rodinpos(train_1_beebook,grd1,internal_element1),identifier(none,b),identifier(none,'OCC')),member(rodinpos(train_1_beebook,grd2,internal_element2),identifier(none,b),domain(none,identifier(none,'TRK'))),not_member(rodinpos(train_1_beebook,grd3,internal_element3),function(none,identifier(none,'TRK'),[identifier(none,b)]),identifier(none,'OCC'))],[],[assign(rodinpos(train_1_beebook,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_1_beebook,'BACK_MOVE_1',internal_element9),'BACK_MOVE_1',ordinary(none),['BACK_MOVE_1'],[identifier(rodinpos(train_1_beebook,[],internal_element1),b)],[member(rodinpos(train_1_beebook,grd1,internal_element1),identifier(none,b),identifier(none,'LBT')),not_member(rodinpos(train_1_beebook,grd2,internal_element2),identifier(none,b),domain(none,identifier(none,'TRK')))],[],[assign(rodinpos(train_1_beebook,act1,internal_element1),[identifier(none,'OCC')],[set_subtraction(none,identifier(none,'OCC'),set_extension(none,[identifier(none,b)]))]),assign(rodinpos(train_1_beebook,act2,internal_element2),[identifier(none,rsrtbl)],[domain_subtraction(none,set_extension(none,[identifier(none,b)]),identifier(none,rsrtbl))]),assign(rodinpos(train_1_beebook,act3,internal_element3),[identifier(none,resbl)],[set_subtraction(none,identifier(none,resbl),set_extension(none,[identifier(none,b)]))]),assign(rodinpos(train_1_beebook,act4,internal_element4),[identifier(none,'LBT')],[set_subtraction(none,identifier(none,'LBT'),set_extension(none,[identifier(none,b)]))])],[]),event(rodinpos(train_1_beebook,'BACK_MOVE_2','internal_element:'),'BACK_MOVE_2',ordinary(none),['BACK_MOVE_2'],[identifier(rodinpos(train_1_beebook,[],internal_element1),b)],[member(rodinpos(train_1_beebook,grd1,internal_element1),identifier(none,b),identifier(none,'LBT')),member(rodinpos(train_1_beebook,grd2,internal_element2),identifier(none,b),domain(none,identifier(none,'TRK'))),member(rodinpos(train_1_beebook,grd3,internal_element3),function(none,identifier(none,'TRK'),[identifier(none,b)]),identifier(none,'OCC'))],[],[assign(rodinpos(train_1_beebook,act1,internal_element1),[identifier(none,'OCC')],[set_subtraction(none,identifier(none,'OCC'),set_extension(none,[identifier(none,b)]))]),assign(rodinpos(train_1_beebook,act2,internal_element2),[identifier(none,rsrtbl)],[domain_subtraction(none,set_extension(none,[identifier(none,b)]),identifier(none,rsrtbl))]),assign(rodinpos(train_1_beebook,act3,internal_element3),[identifier(none,resbl)],[set_subtraction(none,identifier(none,resbl),set_extension(none,[identifier(none,b)]))]),assign(rodinpos(train_1_beebook,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_1_beebook,point_positionning,'internal_element;'),point_positionning,ordinary(none),[point_positionning],[identifier(rodinpos(train_1_beebook,[],internal_element1),r)],[member(rodinpos(train_1_beebook,grd1,internal_element1),identifier(none,r),set_subtraction(none,identifier(none,resrt),identifier(none,frm)))],[],[assign(rodinpos(train_1_beebook,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_beebook,route_formation,'internal_element='),route_formation,ordinary(none),[route_formation],[identifier(rodinpos(train_1_beebook,[],'\''),r)],[member(rodinpos(train_1_beebook,grd1,'('),identifier(none,r),set_subtraction(none,identifier(none,resrt),identifier(none,frm))),equal(rodinpos(train_1_beebook,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_beebook,act1,'*'),[identifier(none,frm)],[union(none,identifier(none,frm),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_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,[])])],[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_ctx0_beebook,'Well-definedness of Axiom',[axiom(compute_rtbl_from_nxt)],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)). +