1

package(load_event_b_project([event_b_model(none,'NQueensAsEvent',[sees(none,[]),variables(none,[identifier(none,n),identifier(none,queens)]),invariant(none,[member(rodinpos(inv1,'_B5snABZEEd-uPJxCRzLqJg'),identifier(none,queens),partial_function(none,interval(none,integer(none,1),identifier(none,n)),interval(none,integer(none,1),identifier(none,n)))),member(rodinpos(i2,'_B5snARZEEd-uPJxCRzLqJg'),identifier(none,n),natural_set(none))]),theorems(none,[]),events(none,[event(rodinpos('INITIALISATION','_B5snAhZEEd-uPJxCRzLqJg'),'INITIALISATION',ordinary(none),[],[],[],[assign(rodinpos(i1,'_B5snAxZEEd-uPJxCRzLqJg'),[identifier(none,queens)],[empty_set(none)]),assign(rodinpos(i2,'_B5snBBZEEd-uPJxCRzLqJg'),[identifier(none,n)],[integer(none,3)])],[]),event(rodinpos(incn,'_B5snBRZEEd-uPJxCRzLqJg'),incn,ordinary(none),[],[],[],[assign(rodinpos(a,'_B5tOEBZEEd-uPJxCRzLqJg'),[identifier(none,n)],[add(none,identifier(none,n),integer(none,1))])],[]),event(rodinpos(solve,'_B5tOERZEEd-uPJxCRzLqJg'),solve,ordinary(none),[],[identifier(rodinpos([],'_B5tOEhZEEd-uPJxCRzLqJg'),q)],[member(rodinpos(axm2,'_B5tOExZEEd-uPJxCRzLqJg'),identifier(none,q),total_bijection(none,interval(none,integer(none,1),identifier(none,n)),interval(none,integer(none,1),identifier(none,n)))),forall(rodinpos(axm3,'_B5tOFBZEEd-uPJxCRzLqJg'),[identifier(none,q1),identifier(none,q2)],implication(none,conjunct(none,member(none,identifier(none,q1),interval(none,integer(none,1),identifier(none,n))),conjunct(none,member(none,identifier(none,q2),interval(none,integer(none,2),identifier(none,n))),greater(none,identifier(none,q2),identifier(none,q1)))),conjunct(none,not_equal(none,minus(none,add(none,function(none,identifier(none,q),[identifier(none,q1)]),identifier(none,q2)),identifier(none,q1)),function(none,identifier(none,q),[identifier(none,q2)])),not_equal(none,add(none,minus(none,function(none,identifier(none,q),[identifier(none,q1)]),identifier(none,q2)),identifier(none,q1)),function(none,identifier(none,q),[identifier(none,q2)])))))],[assign(rodinpos(a,'_B5t1IBZEEd-uPJxCRzLqJg'),[identifier(none,queens)],[identifier(none,q)])],[])])])],[],[discharged('NQueensAsEvent','INITIALISATION',inv1),discharged('NQueensAsEvent','INITIALISATION',i2),discharged('NQueensAsEvent',incn,inv1),discharged('NQueensAsEvent',incn,i2),discharged('NQueensAsEvent',solve,inv1),wp('INITIALISATION',solve,[member(none,identifier(none,q),total_bijection(none,interval(none,integer(none,1),integer(none,3)),interval(none,integer(none,1),integer(none,3)))),forall(none,[identifier(none,q1),identifier(none,q2)],implication(none,conjunct(none,member(none,identifier(none,q1),interval(none,integer(none,1),integer(none,3))),conjunct(none,member(none,identifier(none,q2),interval(none,integer(none,2),integer(none,3))),greater(none,identifier(none,q2),identifier(none,q1)))),conjunct(none,not_equal(none,minus(none,add(none,function(none,identifier(none,q),[identifier(none,q1)]),identifier(none,q2)),identifier(none,q1)),function(none,identifier(none,q),[identifier(none,q2)])),not_equal(none,add(none,minus(none,function(none,identifier(none,q),[identifier(none,q1)]),identifier(none,q2)),identifier(none,q1)),function(none,identifier(none,q),[identifier(none,q2)])))))]),wp(incn,solve,[member(none,identifier(none,q),total_bijection(none,interval(none,integer(none,1),add(none,identifier(none,n),integer(none,1))),interval(none,integer(none,1),add(none,identifier(none,n),integer(none,1))))),forall(none,[identifier(none,q1),identifier(none,q2)],implication(none,conjunct(none,member(none,identifier(none,q1),interval(none,integer(none,1),add(none,identifier(none,n),integer(none,1)))),conjunct(none,member(none,identifier(none,q2),interval(none,integer(none,2),add(none,identifier(none,n),integer(none,1)))),greater(none,identifier(none,q2),identifier(none,q1)))),conjunct(none,not_equal(none,minus(none,add(none,function(none,identifier(none,q),[identifier(none,q1)]),identifier(none,q2)),identifier(none,q1)),function(none,identifier(none,q),[identifier(none,q2)])),not_equal(none,add(none,minus(none,function(none,identifier(none,q),[identifier(none,q1)]),identifier(none,q2)),identifier(none,q1)),function(none,identifier(none,q),[identifier(none,q2)])))))]),nonchanging_guard('INITIALISATION',[]),nonchanging_guard(incn,[]),nonchanging_guard(solve,[member(none,identifier(none,q),total_bijection(none,interval(none,integer(none,1),identifier(none,n)),interval(none,integer(none,1),identifier(none,n)))),forall(none,[identifier(none,q1),identifier(none,q2)],implication(none,conjunct(none,member(none,identifier(none,q1),interval(none,integer(none,1),identifier(none,n))),conjunct(none,member(none,identifier(none,q2),interval(none,integer(none,2),identifier(none,n))),greater(none,identifier(none,q2),identifier(none,q1)))),conjunct(none,not_equal(none,minus(none,add(none,function(none,identifier(none,q),[identifier(none,q1)]),identifier(none,q2)),identifier(none,q1)),function(none,identifier(none,q),[identifier(none,q2)])),not_equal(none,add(none,minus(none,function(none,identifier(none,q),[identifier(none,q1)]),identifier(none,q2)),identifier(none,q1)),function(none,identifier(none,q),[identifier(none,q2)])))))])],Error)).