1		package(load_event_b_project([],[event_b_context(none,'ExplicitComputationsEventB',[extends(none,[]),constants(none,[]),axioms(none,[equal(rodinpos(tot_rel_inv1,'_bJbcAIhCEeCFc6O1QyP73Q'),card(none,total_relation(none,bool_set(none),bool_set(none))),integer(none,9)),equal(rodinpos(tot_rel_inv2,'_bJcDEIhCEeCFc6O1QyP73Q'),card(none,total_relation(none,bool_set(none),interval(none,integer(none,1),integer(none,3)))),integer(none,49)),equal(rodinpos(tot_rel_inv3,'_bJcDEYhCEeCFc6O1QyP73Q'),card(none,total_relation(none,interval(none,integer(none,1),integer(none,0)),interval(none,integer(none,1),integer(none,3)))),integer(none,1)),equal(rodinpos(tot_rel_inv4,'_bJcDEohCEeCFc6O1QyP73Q'),total_relation(none,interval(none,integer(none,1),integer(none,0)),interval(none,integer(none,1),integer(none,3))),set_extension(none,[empty_set(none)])),equal(rodinpos(tot_rel_inv5,'_bJcDE4hCEeCFc6O1QyP73Q'),card(none,total_relation(none,interval(none,integer(none,1),integer(none,3)),interval(none,integer(none,1),integer(none,0)))),integer(none,0)),equal(rodinpos(tot_rel1,'_bJcDFIhCEeCFc6O1QyP73Q'),add(none,card(none,total_relation(none,interval(none,integer(none,1),integer(none,2)),interval(none,integer(none,1),integer(none,2)))),integer(none,1)),card(none,union(none,total_relation(none,interval(none,integer(none,1),integer(none,2)),interval(none,integer(none,1),integer(none,2))),set_extension(none,[set_extension(none,[couple(none,[integer(none,0),integer(none,0)])])])))),equal(rodinpos(tot_rel2,'_bJcDFYhCEeCFc6O1QyP73Q'),add(none,card(none,total_relation(none,interval(none,integer(none,1),integer(none,2)),interval(none,integer(none,1),integer(none,3)))),integer(none,1)),card(none,union(none,total_relation(none,interval(none,integer(none,1),integer(none,2)),interval(none,integer(none,1),integer(none,3))),set_extension(none,[set_extension(none,[couple(none,[integer(none,0),integer(none,0)])])])))),equal(rodinpos(tot_rel3,'_bJcDFohCEeCFc6O1QyP73Q'),add(none,card(none,total_relation(none,interval(none,integer(none,1),integer(none,3)),interval(none,integer(none,1),integer(none,3)))),integer(none,1)),card(none,union(none,total_relation(none,interval(none,integer(none,1),integer(none,3)),interval(none,integer(none,1),integer(none,3))),set_extension(none,[set_extension(none,[couple(none,[integer(none,0),integer(none,0)])])])))),forall(rodinpos(tot_rel_law,'_bJcDF4hCEeCFc6O1QyP73Q'),[identifier(none,n),identifier(none,m)],implication(none,conjunct(none,member(none,identifier(none,n),interval(none,integer(none,0),integer(none,3))),member(none,identifier(none,m),interval(none,integer(none,0),integer(none,3)))),equal(none,add(none,card(none,total_relation(none,interval(none,integer(none,1),identifier(none,n)),interval(none,integer(none,1),identifier(none,m)))),integer(none,1)),card(none,union(none,total_relation(none,interval(none,integer(none,1),identifier(none,n)),interval(none,integer(none,1),identifier(none,m))),set_extension(none,[set_extension(none,[couple(none,[integer(none,0),integer(none,0)])])])))))),forall(rodinpos(surj_rel_law,'_bJcDGIhCEeCFc6O1QyP73Q'),[identifier(none,n),identifier(none,m)],implication(none,conjunct(none,member(none,identifier(none,n),interval(none,integer(none,0),integer(none,3))),member(none,identifier(none,m),interval(none,integer(none,0),integer(none,3)))),equal(none,add(none,card(none,surjection_relation(none,interval(none,integer(none,1),identifier(none,n)),interval(none,integer(none,1),identifier(none,m)))),integer(none,1)),card(none,union(none,surjection_relation(none,interval(none,integer(none,1),identifier(none,n)),interval(none,integer(none,1),identifier(none,m))),set_extension(none,[set_extension(none,[couple(none,[integer(none,0),integer(none,0)])])])))))),forall(rodinpos(tot_surj_rel_law,'_bJcqIIhCEeCFc6O1QyP73Q'),[identifier(none,n),identifier(none,m)],implication(none,conjunct(none,member(none,identifier(none,n),interval(none,integer(none,0),integer(none,3))),member(none,identifier(none,m),interval(none,integer(none,0),integer(none,3)))),equal(none,add(none,card(none,total_surjection_relation(none,interval(none,integer(none,1),identifier(none,n)),interval(none,integer(none,1),identifier(none,m)))),integer(none,1)),card(none,union(none,total_surjection_relation(none,interval(none,integer(none,1),identifier(none,n)),interval(none,integer(none,1),identifier(none,m))),set_extension(none,[set_extension(none,[couple(none,[integer(none,0),integer(none,0)])])]))))))]),theorems(none,[]),sets(none,[])]),event_b_context(none,'ExplicitComputationsEventB',[extends(none,[]),constants(none,[]),axioms(none,[equal(rodinpos(tot_rel_inv1,'_bJbcAIhCEeCFc6O1QyP73Q'),card(none,total_relation(none,bool_set(none),bool_set(none))),integer(none,9)),equal(rodinpos(tot_rel_inv2,'_bJcDEIhCEeCFc6O1QyP73Q'),card(none,total_relation(none,bool_set(none),interval(none,integer(none,1),integer(none,3)))),integer(none,49)),equal(rodinpos(tot_rel_inv3,'_bJcDEYhCEeCFc6O1QyP73Q'),card(none,total_relation(none,interval(none,integer(none,1),integer(none,0)),interval(none,integer(none,1),integer(none,3)))),integer(none,1)),equal(rodinpos(tot_rel_inv4,'_bJcDEohCEeCFc6O1QyP73Q'),total_relation(none,interval(none,integer(none,1),integer(none,0)),interval(none,integer(none,1),integer(none,3))),set_extension(none,[empty_set(none)])),equal(rodinpos(tot_rel_inv5,'_bJcDE4hCEeCFc6O1QyP73Q'),card(none,total_relation(none,interval(none,integer(none,1),integer(none,3)),interval(none,integer(none,1),integer(none,0)))),integer(none,0)),equal(rodinpos(tot_rel1,'_bJcDFIhCEeCFc6O1QyP73Q'),add(none,card(none,total_relation(none,interval(none,integer(none,1),integer(none,2)),interval(none,integer(none,1),integer(none,2)))),integer(none,1)),card(none,union(none,total_relation(none,interval(none,integer(none,1),integer(none,2)),interval(none,integer(none,1),integer(none,2))),set_extension(none,[set_extension(none,[couple(none,[integer(none,0),integer(none,0)])])])))),equal(rodinpos(tot_rel2,'_bJcDFYhCEeCFc6O1QyP73Q'),add(none,card(none,total_relation(none,interval(none,integer(none,1),integer(none,2)),interval(none,integer(none,1),integer(none,3)))),integer(none,1)),card(none,union(none,total_relation(none,interval(none,integer(none,1),integer(none,2)),interval(none,integer(none,1),integer(none,3))),set_extension(none,[set_extension(none,[couple(none,[integer(none,0),integer(none,0)])])])))),equal(rodinpos(tot_rel3,'_bJcDFohCEeCFc6O1QyP73Q'),add(none,card(none,total_relation(none,interval(none,integer(none,1),integer(none,3)),interval(none,integer(none,1),integer(none,3)))),integer(none,1)),card(none,union(none,total_relation(none,interval(none,integer(none,1),integer(none,3)),interval(none,integer(none,1),integer(none,3))),set_extension(none,[set_extension(none,[couple(none,[integer(none,0),integer(none,0)])])])))),forall(rodinpos(tot_rel_law,'_bJcDF4hCEeCFc6O1QyP73Q'),[identifier(none,n),identifier(none,m)],implication(none,conjunct(none,member(none,identifier(none,n),interval(none,integer(none,0),integer(none,3))),member(none,identifier(none,m),interval(none,integer(none,0),integer(none,3)))),equal(none,add(none,card(none,total_relation(none,interval(none,integer(none,1),identifier(none,n)),interval(none,integer(none,1),identifier(none,m)))),integer(none,1)),card(none,union(none,total_relation(none,interval(none,integer(none,1),identifier(none,n)),interval(none,integer(none,1),identifier(none,m))),set_extension(none,[set_extension(none,[couple(none,[integer(none,0),integer(none,0)])])])))))),forall(rodinpos(surj_rel_law,'_bJcDGIhCEeCFc6O1QyP73Q'),[identifier(none,n),identifier(none,m)],implication(none,conjunct(none,member(none,identifier(none,n),interval(none,integer(none,0),integer(none,3))),member(none,identifier(none,m),interval(none,integer(none,0),integer(none,3)))),equal(none,add(none,card(none,surjection_relation(none,interval(none,integer(none,1),identifier(none,n)),interval(none,integer(none,1),identifier(none,m)))),integer(none,1)),card(none,union(none,surjection_relation(none,interval(none,integer(none,1),identifier(none,n)),interval(none,integer(none,1),identifier(none,m))),set_extension(none,[set_extension(none,[couple(none,[integer(none,0),integer(none,0)])])])))))),forall(rodinpos(tot_surj_rel_law,'_bJcqIIhCEeCFc6O1QyP73Q'),[identifier(none,n),identifier(none,m)],implication(none,conjunct(none,member(none,identifier(none,n),interval(none,integer(none,0),integer(none,3))),member(none,identifier(none,m),interval(none,integer(none,0),integer(none,3)))),equal(none,add(none,card(none,total_surjection_relation(none,interval(none,integer(none,1),identifier(none,n)),interval(none,integer(none,1),identifier(none,m)))),integer(none,1)),card(none,union(none,total_surjection_relation(none,interval(none,integer(none,1),identifier(none,n)),interval(none,integer(none,1),identifier(none,m))),set_extension(none,[set_extension(none,[couple(none,[integer(none,0),integer(none,0)])])]))))))]),theorems(none,[]),sets(none,[])])],[],_Error)).
2