1		package(load_event_b_project([],[event_b_context(none,testSUM,[extends(none,[]),constants(none,[identifier(none,agg_op1),identifier(none,agg_op2),identifier(none,x)]),abstract_constants(none,[]),axioms(none,[equal(rodinpos(testSUM,axm1,'__tZmUyK7EeS6V7rzo1PjRw'),identifier(none,x),set_extension(none,[couple(none,[integer(none,1),integer(none,2)]),couple(none,[integer(none,2),integer(none,3)])])),conjunct(rodinpos(testSUM,axm2,'__taNYSK7EeS6V7rzo1PjRw'),equal(none,identifier(none,agg_op1),integer(none,1)),equal(none,identifier(none,agg_op2),integer(none,2)))]),theorems(none,[equal(rodinpos(testSUM,thm1,'__taNYCK7EeS6V7rzo1PjRw'),typeof(none,extended_expr(none,'SUM',[identifier(none,x)],[]),integer_set(none)),integer(none,5)),equal(rodinpos(testSUM,thm2,'__taNYiK7EeS6V7rzo1PjRw'),typeof(none,extended_expr(none,'SUM',[set_extension(none,[couple(none,[integer(none,1),identifier(none,agg_op1)]),couple(none,[integer(none,2),identifier(none,agg_op2)])])],[]),integer_set(none)),integer(none,3))]),sets(none,[])])],[exporter_version(3),po(testSUM,'Well-definedness of Theorem',[axiom(thm1)],false),po(testSUM,'Theorem',[axiom(thm1)],false),po(testSUM,'Well-definedness of Theorem',[axiom(thm2)],false),po(testSUM,'Theorem',[axiom(thm2)],false),theory(theory_name('SUM','SUMandPRODUCT'),[],['T'],[],[],[axiomatic_def_block(xdb1,[],[opdef('SUM',[argument(s,pow_subset(none,cartesian_product(none,identifier(none,'T'),integer_set(none))))],[]),opdef('PRODUCT',[argument(s,pow_subset(none,cartesian_product(none,identifier(none,'T'),integer_set(none))))],[])],[equal(none,typeof(none,extended_expr(none,'SUM',[event_b_comprehension_set(none,[identifier(none,p)],identifier(none,p),conjunct(none,member(none,identifier(none,p),cartesian_product(none,identifier(none,'T'),integer_set(none))),conjunct(none,member(none,identifier(none,p),cartesian_product(none,identifier(none,'T'),integer_set(none))),falsity(none))))],[]),integer_set(none)),integer(none,0)),forall(none,[identifier(none,t),identifier(none,x)],implication(none,conjunct(none,member(none,identifier(none,t),identifier(none,'T')),conjunct(none,member(none,identifier(none,x),integer_set(none)),conjunct(none,member(none,identifier(none,t),identifier(none,'T')),member(none,identifier(none,x),integer_set(none))))),equal(none,typeof(none,extended_expr(none,'SUM',[set_extension(none,[couple(none,[identifier(none,t),identifier(none,x)])])],[]),integer_set(none)),identifier(none,x)))),forall(none,[identifier(none,s),identifier(none,t)],implication(none,conjunct(none,member(none,identifier(none,s),pow_subset(none,cartesian_product(none,identifier(none,'T'),integer_set(none)))),conjunct(none,member(none,identifier(none,t),pow_subset(none,cartesian_product(none,identifier(none,'T'),integer_set(none)))),conjunct(none,member(none,identifier(none,s),partial_function(none,identifier(none,'T'),integer_set(none))),conjunct(none,member(none,identifier(none,t),partial_function(none,identifier(none,'T'),integer_set(none))),conjunct(none,finite(none,identifier(none,s)),conjunct(none,finite(none,identifier(none,t)),equal(none,intersection(none,domain(none,identifier(none,s)),domain(none,identifier(none,t))),typeof(none,empty_set(none),pow_subset(none,identifier(none,'T')))))))))),equal(none,typeof(none,extended_expr(none,'SUM',[union(none,identifier(none,s),identifier(none,t))],[]),integer_set(none)),add(none,typeof(none,extended_expr(none,'SUM',[identifier(none,s)],[]),integer_set(none)),typeof(none,extended_expr(none,'SUM',[identifier(none,t)],[]),integer_set(none)))))),equal(none,typeof(none,extended_expr(none,'PRODUCT',[event_b_comprehension_set(none,[identifier(none,p)],identifier(none,p),conjunct(none,member(none,identifier(none,p),cartesian_product(none,identifier(none,'T'),integer_set(none))),conjunct(none,member(none,identifier(none,p),cartesian_product(none,identifier(none,'T'),integer_set(none))),falsity(none))))],[]),integer_set(none)),integer(none,1)),forall(none,[identifier(none,t),identifier(none,x)],implication(none,conjunct(none,member(none,identifier(none,t),identifier(none,'T')),conjunct(none,member(none,identifier(none,x),integer_set(none)),conjunct(none,member(none,identifier(none,t),identifier(none,'T')),member(none,identifier(none,x),integer_set(none))))),equal(none,typeof(none,extended_expr(none,'PRODUCT',[set_extension(none,[couple(none,[identifier(none,t),identifier(none,x)])])],[]),integer_set(none)),identifier(none,x)))),forall(none,[identifier(none,s),identifier(none,t)],implication(none,conjunct(none,member(none,identifier(none,s),pow_subset(none,cartesian_product(none,identifier(none,'T'),integer_set(none)))),conjunct(none,member(none,identifier(none,t),pow_subset(none,cartesian_product(none,identifier(none,'T'),integer_set(none)))),conjunct(none,member(none,identifier(none,s),partial_function(none,identifier(none,'T'),integer_set(none))),conjunct(none,member(none,identifier(none,t),partial_function(none,identifier(none,'T'),integer_set(none))),conjunct(none,finite(none,identifier(none,s)),conjunct(none,finite(none,identifier(none,t)),equal(none,intersection(none,domain(none,identifier(none,s)),domain(none,identifier(none,t))),typeof(none,empty_set(none),pow_subset(none,identifier(none,'T')))))))))),equal(none,typeof(none,extended_expr(none,'PRODUCT',[union(none,identifier(none,s),identifier(none,t))],[]),integer_set(none)),multiplication(none,typeof(none,extended_expr(none,'PRODUCT',[identifier(none,s)],[]),integer_set(none)),typeof(none,extended_expr(none,'PRODUCT',[identifier(none,t)],[]),integer_set(none))))))])],[tag('SUM','SIGMA'),tag('PRODUCT','PI')])],_Error)).
2