1		package(load_event_b_project([event_b_model(none,'TheoremInGuardError',[sees(none,[]),variables(none,[identifier(none,x)]),invariant(none,[member(rodinpos('TheoremInGuardError',inv,'_c0yxouStEeaU86Rx_hNGRg'),identifier(none,x),natural_set(none))]),theorems(none,[]),variant(none,identifier(none,x)),events(none,[event(rodinpos('TheoremInGuardError','INITIALISATION','\''),'INITIALISATION',ordinary(none),[],[],[],[],[assign(rodinpos('TheoremInGuardError',ini,'_c0yxoOStEeaU86Rx_hNGRg'),[identifier(none,x)],[integer(none,20)])],[]),event(rodinpos('TheoremInGuardError',dec,'_c0yxpOStEeaU86Rx_hNGRg'),dec,convergent(none),[],[],[greater(rodinpos('TheoremInGuardError',g1,'_c0yxpeStEeaU86Rx_hNGRg'),identifier(none,x),integer(none,0))],[not_equal(rodinpos('TheoremInGuardError',thm1,'_c0yxpuStEeaU86Rx_hNGRg'),identifier(none,x),integer(none,2))],[assign(rodinpos('TheoremInGuardError',d,'_c0yxp-StEeaU86Rx_hNGRg'),[identifier(none,x)],[minus(none,identifier(none,x),integer(none,1))])],[])])])],[],[exporter_version(3),po('TheoremInGuardError','Invariant establishment',[event('INITIALISATION'),invariant(inv)],false),po('TheoremInGuardError','Theorem',[guard(thm1),event(dec)],false),po('TheoremInGuardError','Invariant preservation',[event(dec),invariant(inv)],false),po('TheoremInGuardError','Variant of event',[variant('TheoremInGuardError'),event(dec)],false),po('TheoremInGuardError','Natural number variant of event',[variant('TheoremInGuardError'),event(dec)],false)],_Error)).
2