1		package(load_event_b_project([],[event_b_context(none,c0,[extends(none,[]),constants(none,[identifier(none,'S'),identifier(none,'T')]),abstract_constants(none,[]),axioms(none,[member(rodinpos(c0,'S_type','+'),identifier(none,'S'),pow_subset(none,identifier(none,'X'))),member(rodinpos(c0,'T_type','-'),identifier(none,'T'),pow_subset(none,identifier(none,'X')))]),theorems(none,[equal(rodinpos(c0,thm1,')'),general_union(none,set_extension(none,[identifier(none,'S'),identifier(none,'T')])),union(none,identifier(none,'S'),identifier(none,'T'))),equal(rodinpos(c0,thm2,'('),quantified_union(none,[identifier(none,x)],subset(none,identifier(none,x),identifier(none,'X')),identifier(none,x)),identifier(none,'X')),equal(rodinpos(c0,thm3,'.'),general_intersection(none,set_extension(none,[identifier(none,'S'),identifier(none,'T')])),intersection(none,identifier(none,'S'),identifier(none,'T'))),equal(rodinpos(c0,thm4,'/'),quantified_intersection(none,[identifier(none,x)],subset(none,identifier(none,x),identifier(none,'X')),identifier(none,x)),empty_set(none)),equal(rodinpos(c0,thm5b,'_t2IOMDAVEeO9RLemeliDQA'),quantified_union(none,[identifier(none,x)],member(none,identifier(none,x),interval(none,integer(none,1),integer(none,999))),set_extension(none,[multiplication(none,integer(none,2),identifier(none,x))])),event_b_comprehension_set(none,[identifier(none,y)],multiplication(none,integer(none,2),identifier(none,y)),member(none,identifier(none,y),interval(none,integer(none,1),integer(none,999)))))]),sets(none,[deferred_set(none,'X')])])],[exporter_version(3),po(c0,'Theorem',[axiom(thm1)],true),po(c0,'Theorem',[axiom(thm2)],true),po(c0,'Well-definedness of Theorem',[axiom(thm3)],true),po(c0,'Theorem',[axiom(thm3)],true),po(c0,'Well-definedness of Theorem',[axiom(thm4)],true),po(c0,'Theorem',[axiom(thm4)],true),po(c0,'Theorem',[axiom(thm5b)],false)],_Error)).
2