1		package(load_event_b_project([event_b_model(none,'TestWDProblems',[sees(none,[]),variables(none,[identifier(none,f),identifier(none,x)]),invariant(none,[member(rodinpos(inv,'_orb7sZfpEeCTU6xQiIvIkA'),identifier(none,f),partial_function(none,natural_set(none),natural_set(none))),member(rodinpos(invx,'_orb7spfpEeCTU6xQiIvIkA'),identifier(none,x),natural_set(none))]),theorems(none,[]),events(none,[event(rodinpos('INITIALISATION','\''),'INITIALISATION',ordinary(none),[],[],[],[],[assign(rodinpos(ini,'_orciwJfpEeCTU6xQiIvIkA'),[identifier(none,f),identifier(none,x)],[set_extension(none,[couple(none,[integer(none,1),integer(none,2)]),couple(none,[integer(none,2),integer(none,4)]),couple(none,[integer(none,3),integer(none,6)]),couple(none,[integer(none,3),integer(none,7)])]),integer(none,1)])],[]),event(rodinpos(applyf,'_orciwZfpEeCTU6xQiIvIkA'),applyf,ordinary(none),[],[],[],[],[assign(rodinpos(app,'_orciwpfpEeCTU6xQiIvIkA'),[identifier(none,x)],[function(none,identifier(none,f),[identifier(none,x)])])],[]),event(rodinpos(incx,'_orciw5fpEeCTU6xQiIvIkA'),incx,ordinary(none),[],[],[],[],[assign(rodinpos(inc,'_ordJ0JfpEeCTU6xQiIvIkA'),[identifier(none,x)],[add(none,identifier(none,x),integer(none,1))])],[]),event(rodinpos(divby0,'_ordJ0ZfpEeCTU6xQiIvIkA'),divby0,ordinary(none),[],[],[],[],[assign(rodinpos(div,'_ordJ0pfpEeCTU6xQiIvIkA'),[identifier(none,x)],[div(none,identifier(none,x),integer(none,0))])],[])])])],[],[discharged('TestWDProblems','INITIALISATION',invx),discharged('TestWDProblems',applyf,invx),discharged('TestWDProblems',incx,invx),discharged('TestWDProblems',divby0,invx)],_Error)).
2