1		package(load_event_b_project([event_b_model(none,'NonDetAssign1_finite_unproven',[sees(none,[]),refines(none,'NonDetAssign0'),variables(none,[identifier(none,y)]),invariant(none,[equal(rodinpos('NonDetAssign1_finite_unproven',invy,'_9IAGBOR7EeaU86Rx_hNGRg'),identifier(none,y),add(none,identifier(none,x),integer(none,1))),less(rodinpos('NonDetAssign1_finite_unproven',invy2,'_HJDUMeR8EeaU86Rx_hNGRg'),identifier(none,y),integer(none,100))]),theorems(none,[]),events(none,[event(rodinpos('NonDetAssign1_finite_unproven','INITIALISATION','\''),'INITIALISATION',ordinary(none),['INITIALISATION'],[],[],[],[assign(rodinpos('NonDetAssign1_finite_unproven',ini,'_9IAGAuR7EeaU86Rx_hNGRg'),[identifier(none,y)],[integer(none,2)])],[witness(none,identifier(none,'x\''),equal(rodinpos('NonDetAssign1_finite_unproven','x\'','_9IAGAeR7EeaU86Rx_hNGRg'),identifier(none,'x\''),integer(none,1)))]),event(rodinpos('NonDetAssign1_finite_unproven',inc,'_9IAGBeR7EeaU86Rx_hNGRg'),inc,ordinary(none),[inc],[],[less(rodinpos('NonDetAssign1_finite_unproven',g2,'_9IAtFeR7EeaU86Rx_hNGRg'),identifier(none,y),integer(none,98))],[],[becomes_element_of(rodinpos('NonDetAssign1_finite_unproven',incx,'_9IAtEuR7EeaU86Rx_hNGRg'),[identifier(none,y)],set_extension(none,[add(none,identifier(none,y),integer(none,1)),add(none,identifier(none,y),integer(none,2))]))],[witness(none,identifier(none,'x\''),equal(rodinpos('NonDetAssign1_finite_unproven','x\'','_9IAtEeR7EeaU86Rx_hNGRg'),identifier(none,'x\''),minus(none,identifier(none,'y\''),integer(none,1))))]),event(rodinpos('NonDetAssign1_finite_unproven',odd,'_9IAtE-R7EeaU86Rx_hNGRg'),odd,ordinary(none),[odd],[],[equal(rodinpos('NonDetAssign1_finite_unproven',g,'_9IAtGuR7EeaU86Rx_hNGRg'),modulo(none,identifier(none,y),integer(none,2)),integer(none,0))],[],[assign(rodinpos('NonDetAssign1_finite_unproven',dec,'_9IAtFuR7EeaU86Rx_hNGRg'),[identifier(none,y)],[minus(none,identifier(none,y),integer(none,1))])],[]),event(rodinpos('NonDetAssign1_finite_unproven',half,'_9IAtF-R7EeaU86Rx_hNGRg'),half,ordinary(none),[half],[identifier(rodinpos('NonDetAssign1_finite_unproven',[],'_9IAtGeR7EeaU86Rx_hNGRg'),h)],[conjunct(rodinpos('NonDetAssign1_finite_unproven',g,'_HJDUMOR8EeaU86Rx_hNGRg'),equal(none,identifier(none,h),div(none,minus(none,identifier(none,y),integer(none,1)),integer(none,2))),greater(none,identifier(none,h),integer(none,0)))],[],[assign(rodinpos('NonDetAssign1_finite_unproven',h,'_9IAtG-R7EeaU86Rx_hNGRg'),[identifier(none,y)],[add(none,identifier(none,h),integer(none,1))])],[])])]),event_b_model(none,'NonDetAssign0',[sees(none,[]),variables(none,[identifier(none,x)]),invariant(none,[member(rodinpos('NonDetAssign0',inv1,'_v06WweRkEeaU86Rx_hNGRg'),identifier(none,x),natural_set(none))]),theorems(none,[]),events(none,[event(rodinpos('NonDetAssign0','INITIALISATION','\''),'INITIALISATION',ordinary(none),[],[],[],[],[becomes_element_of(rodinpos('NonDetAssign0',ini,'_v05vsORkEeaU86Rx_hNGRg'),[identifier(none,x)],interval(none,integer(none,0),integer(none,2)))],[]),event(rodinpos('NonDetAssign0',inc,'_v06WwuRkEeaU86Rx_hNGRg'),inc,ordinary(none),[],[],[],[],[becomes_element_of(rodinpos('NonDetAssign0',incx,'_v06Ww-RkEeaU86Rx_hNGRg'),[identifier(none,x)],set_extension(none,[add(none,identifier(none,x),integer(none,1)),add(none,identifier(none,x),integer(none,2))]))],[]),event(rodinpos('NonDetAssign0',odd,'_v06WxORkEeaU86Rx_hNGRg'),odd,ordinary(none),[],[],[equal(rodinpos('NonDetAssign0',g,'_v06WxeRkEeaU86Rx_hNGRg'),modulo(none,identifier(none,x),integer(none,2)),integer(none,1))],[],[assign(rodinpos('NonDetAssign0',dec,'_v06WxuRkEeaU86Rx_hNGRg'),[identifier(none,x)],[minus(none,identifier(none,x),integer(none,1))])],[]),event(rodinpos('NonDetAssign0',half,'_v0690ORkEeaU86Rx_hNGRg'),half,ordinary(none),[],[identifier(rodinpos('NonDetAssign0',[],'_v08L8ORkEeaU86Rx_hNGRg'),h)],[conjunct(rodinpos('NonDetAssign0',g,'_v08L8eRkEeaU86Rx_hNGRg'),equal(none,identifier(none,h),div(none,identifier(none,x),integer(none,2))),greater(none,identifier(none,h),integer(none,0)))],[],[assign(rodinpos('NonDetAssign0',h,'_v08L8uRkEeaU86Rx_hNGRg'),[identifier(none,x)],[identifier(none,h)])],[])])])],[],[exporter_version(3),po('NonDetAssign1_finite_unproven','Invariant establishment',[event('INITIALISATION'),event('INITIALISATION'),invariant(invy)],false),po('NonDetAssign1_finite_unproven','Invariant establishment',[event('INITIALISATION'),event('INITIALISATION'),invariant(invy2)],false),po('NonDetAssign1_finite_unproven','Action simulation',[event('INITIALISATION'),action(ini),event('INITIALISATION')],false),po('NonDetAssign1_finite_unproven','Invariant preservation',[event(inc),event(inc),invariant(invy)],false),po('NonDetAssign1_finite_unproven','Invariant preservation',[event(inc),event(inc),invariant(invy2)],false),po('NonDetAssign1_finite_unproven','Feasibility of action',[action(incx)],false),po('NonDetAssign1_finite_unproven','Action simulation',[event(inc),action(incx),event(inc)],false),po('NonDetAssign1_finite_unproven','Well-definedness of Guard',[guard(g),event(odd)],false),po('NonDetAssign1_finite_unproven','Invariant preservation',[event(odd),event(odd),invariant(invy)],false),po('NonDetAssign1_finite_unproven','Invariant preservation',[event(odd),event(odd),invariant(invy2)],false),po('NonDetAssign1_finite_unproven','Guard strengthening (split)',[event(odd),guard(g),event(odd),event(odd)],false),po('NonDetAssign1_finite_unproven','Well-definedness of Guard',[guard(g),event(half)],false),po('NonDetAssign1_finite_unproven','Invariant preservation',[event(half),event(half),invariant(invy)],false),po('NonDetAssign1_finite_unproven','Invariant preservation',[event(half),event(half),invariant(invy2)],false),po('NonDetAssign1_finite_unproven','Guard strengthening (split)',[event(half),guard(g),event(half),event(half)],false),po('NonDetAssign0','Invariant establishment',[event('INITIALISATION'),invariant(inv1)],false),po('NonDetAssign0','Feasibility of action',[action(ini)],false),po('NonDetAssign0','Invariant preservation',[event(inc),invariant(inv1)],false),po('NonDetAssign0','Feasibility of action',[action(incx)],false),po('NonDetAssign0','Well-definedness of Guard',[guard(g),event(odd)],false),po('NonDetAssign0','Invariant preservation',[event(odd),invariant(inv1)],false),po('NonDetAssign0','Well-definedness of Guard',[guard(g),event(half)],false),po('NonDetAssign0','Invariant preservation',[event(half),invariant(inv1)],false)],_Error)).
2