1		package(load_event_b_project([],[event_b_context(none,'TestHilbert',[extends(none,[]),constants(none,[]),abstract_constants(none,[]),axioms(none,[]),theorems(none,[equal(rodinpos('TestHilbert',thm1,'\''),typeof(none,extended_expr(none,choose,[set_extension(none,[integer(none,1)])],[]),integer_set(none)),integer(none,1)),member(rodinpos('TestHilbert',thm2,'('),typeof(none,extended_expr(none,choose,[set_extension(none,[integer(none,1),integer(none,3)])],[]),integer_set(none)),interval(none,integer(none,1),integer(none,3))),equal(rodinpos('TestHilbert',thm3,')'),typeof(none,extended_expr(none,choose,[set_extension(none,[integer(none,1),integer(none,2)])],[]),integer_set(none)),typeof(none,extended_expr(none,choose,[set_extension(none,[integer(none,2),integer(none,1)])],[]),integer_set(none)))]),sets(none,[])])],[exporter_version(3),po('TestHilbert','Well-definedness of Theorem',[axiom(thm1)],true),po('TestHilbert','Theorem',[axiom(thm1)],true),po('TestHilbert','Well-definedness of Theorem',[axiom(thm2)],true),po('TestHilbert','Theorem',[axiom(thm2)],true),po('TestHilbert','Well-definedness of Theorem',[axiom(thm3)],true),po('TestHilbert','Theorem',[axiom(thm3)],true),theory(theory_name('Theories',if_then_else),[],['A'],[],[operator(if,[argument(test,bool_set(none)),argument(then,identifier(none,'A')),argument(else,identifier(none,'A'))],conjunct(none,forall(none,[identifier(none,x)],implication(none,member(none,identifier(none,x),bool_set(none)),disjunct(none,conjunct(none,member(none,identifier(none,x),bool_set(none)),equal(none,identifier(none,test),boolean_true(none))),disjunct(none,negation(none,member(none,identifier(none,x),bool_set(none))),negation(none,equal(none,identifier(none,test),boolean_true(none))))))),conjunct(none,forall(none,[identifier(none,x)],implication(none,member(none,identifier(none,x),bool_set(none)),disjunct(none,conjunct(none,member(none,identifier(none,x),bool_set(none)),equal(none,identifier(none,test),boolean_false(none))),disjunct(none,negation(none,member(none,identifier(none,x),bool_set(none))),negation(none,equal(none,identifier(none,test),boolean_false(none))))))),conjunct(none,member(none,boolean_true(none),domain(none,union(none,event_b_comprehension_set(none,[identifier(none,x)],couple(none,[identifier(none,x),identifier(none,then)]),conjunct(none,member(none,identifier(none,x),bool_set(none)),conjunct(none,member(none,identifier(none,x),bool_set(none)),equal(none,identifier(none,test),boolean_true(none))))),event_b_comprehension_set(none,[identifier(none,x)],couple(none,[identifier(none,x),identifier(none,else)]),conjunct(none,member(none,identifier(none,x),bool_set(none)),conjunct(none,member(none,identifier(none,x),bool_set(none)),equal(none,identifier(none,test),boolean_false(none)))))))),member(none,union(none,event_b_comprehension_set(none,[identifier(none,x)],couple(none,[identifier(none,x),identifier(none,then)]),conjunct(none,member(none,identifier(none,x),bool_set(none)),conjunct(none,member(none,identifier(none,x),bool_set(none)),equal(none,identifier(none,test),boolean_true(none))))),event_b_comprehension_set(none,[identifier(none,x)],couple(none,[identifier(none,x),identifier(none,else)]),conjunct(none,member(none,identifier(none,x),bool_set(none)),conjunct(none,member(none,identifier(none,x),bool_set(none)),equal(none,identifier(none,test),boolean_false(none)))))),partial_function(none,bool_set(none),identifier(none,'A')))))),[function(none,union(none,event_b_comprehension_set(none,[identifier(none,x)],couple(none,[identifier(none,x),identifier(none,then)]),conjunct(none,member(none,identifier(none,x),bool_set(none)),conjunct(none,member(none,identifier(none,x),bool_set(none)),equal(none,identifier(none,test),boolean_true(none))))),event_b_comprehension_set(none,[identifier(none,x)],couple(none,[identifier(none,x),identifier(none,else)]),conjunct(none,member(none,identifier(none,x),bool_set(none)),conjunct(none,member(none,identifier(none,x),bool_set(none)),equal(none,identifier(none,test),boolean_false(none)))))),[boolean_true(none)])],[])],[],[]),theory(theory_name('Theories','Cond_IFT'),[],['A'],[],[operator(ifte,[argument('Test',bool_set(none)),argument('Then',identifier(none,'A')),argument('Else',identifier(none,'A'))],conjunct(none,truth(none),conjunct(none,implication(none,equal(none,identifier(none,'Test'),boolean_true(none)),truth(none)),implication(none,negation(none,equal(none,identifier(none,'Test'),boolean_true(none))),truth(none)))),[typeof(none,extended_expr(none,'COND',[identifier(none,'Then'),identifier(none,'Else')],[equal(none,identifier(none,'Test'),boolean_true(none))]),identifier(none,'A'))],[])],[],[]),theory(theory_name('Theories','HilbertChoose'),[],['A'],[],[],[axiomatic_def_block(chooseAxioms,[],[opdef(choose,[argument('S',pow_subset(none,identifier(none,'A')))],[])],[forall(none,[identifier(none,'SS')],implication(none,conjunct(none,member(none,identifier(none,'SS'),pow_subset(none,identifier(none,'A'))),subset(none,identifier(none,'SS'),identifier(none,'A'))),member(none,typeof(none,extended_expr(none,choose,[identifier(none,'SS')],[]),identifier(none,'A')),identifier(none,'SS'))))])],[tag(choose,choose)])],_Error)).
2