1		package(load_event_b_project([event_b_model(none,'SET_GAM_Sym_NoSet20',[sees(none,['SET_Sym_Context']),variables(none,[identifier(none,cards),identifier(none,n)]),invariant(none,[member(rodinpos(ninv,'_Dh1mw19dEeCktKroT8lBpg'),identifier(none,n),interval(none,integer(none,0),integer(none,21))),member(rodinpos(cards,'_Dh1mxF9dEeCktKroT8lBpg'),identifier(none,cards),total_function(none,interval(none,integer(none,1),identifier(none,n)),total_function(none,identifier(none,'ATTR'),identifier(none,'VAL'))))]),theorems(none,[]),events(none,[event(rodinpos('INITIALISATION','\''),'INITIALISATION',ordinary(none),[],[],[],[],[assign(rodinpos(i,'_Dh2N0F9dEeCktKroT8lBpg'),[identifier(none,cards),identifier(none,n)],[empty_set(none),integer(none,0)])],[]),event(rodinpos(addcard,'_Dh2N0V9dEeCktKroT8lBpg'),addcard,ordinary(none),[],[identifier(rodinpos([],'_Dh2N0l9dEeCktKroT8lBpg'),i),identifier(rodinpos([],'_Dh2N019dEeCktKroT8lBpg'),newcard)],[conjunct(rodinpos(guard,'_Dh2N1F9dEeCktKroT8lBpg'),equal(none,identifier(none,i),add(none,identifier(none,n),integer(none,1))),less_equal(none,identifier(none,i),integer(none,21))),member(rodinpos(cardg,'_Dh2N1V9dEeCktKroT8lBpg'),identifier(none,newcard),total_function(none,identifier(none,'ATTR'),identifier(none,'VAL'))),not_member(rodinpos(new,'_Dh204F9dEeCktKroT8lBpg'),identifier(none,newcard),range(none,identifier(none,cards))),forall(rodinpos(noset,'_Dh204V9dEeCktKroT8lBpg'),[identifier(none,j),identifier(none,k)],implication(none,conjunct(none,greater(none,identifier(none,j),integer(none,0)),conjunct(none,less(none,identifier(none,j),identifier(none,k)),less(none,identifier(none,k),identifier(none,i)))),exists(none,[identifier(none,s)],implication(none,member(none,identifier(none,s),identifier(none,'ATTR')),equal(none,card(none,set_extension(none,[function(none,identifier(none,newcard),[identifier(none,s)]),function(none,function(none,identifier(none,cards),[identifier(none,j)]),[identifier(none,s)]),function(none,function(none,identifier(none,cards),[identifier(none,k)]),[identifier(none,s)])])),integer(none,2))))))],[],[assign(rodinpos(act1,'_Dh204l9dEeCktKroT8lBpg'),[identifier(none,n)],[identifier(none,i)]),assign(rodinpos(cact1,'_Dh20419dEeCktKroT8lBpg'),[identifier(none,cards)],[overwrite(none,identifier(none,cards),set_extension(none,[couple(none,[identifier(none,i),identifier(none,newcard)])]))])],[]),event(rodinpos(eq18,'_Dh205F9dEeCktKroT8lBpg'),eq18,ordinary(none),[],[],[equal(rodinpos(guard,'_Dh3b8F9dEeCktKroT8lBpg'),identifier(none,n),integer(none,18))],[],[],[]),event(rodinpos(eq19,'_Dh3b8V9dEeCktKroT8lBpg'),eq19,ordinary(none),[],[],[equal(rodinpos(guard,'_Dh3b8l9dEeCktKroT8lBpg'),identifier(none,n),integer(none,19))],[],[],[]),event(rodinpos(lt20,'_Dh3b819dEeCktKroT8lBpg'),lt20,ordinary(none),[],[],[less(rodinpos(guard,'_Dh3b9F9dEeCktKroT8lBpg'),identifier(none,n),integer(none,20))],[],[],[])])])],[event_b_context(none,'SET_Sym_Context',[extends(none,[]),constants(none,[identifier(none,'NrC')]),axioms(none,[equal(rodinpos(c3,'_dChSg17rEeCktKroT8lBpg'),card(none,identifier(none,'VAL')),integer(none,3)),equal(rodinpos(c4,'_dCh5kF7rEeCktKroT8lBpg'),card(none,identifier(none,'ATTR')),integer(none,4)),equal(rodinpos(nrc,'_dCh5kV7rEeCktKroT8lBpg'),identifier(none,'NrC'),integer(none,12))]),theorems(none,[]),sets(none,[deferred_set(none,'ATTR'),deferred_set(none,'VAL')])])],[discharged('SET_GAM_Sym_NoSet20','INITIALISATION',ninv),discharged('SET_GAM_Sym_NoSet20','INITIALISATION',cards),discharged('SET_GAM_Sym_NoSet20',addcard,ninv),discharged('SET_GAM_Sym_NoSet20',addcard,cards)],_Error)).
2