1 package(load_event_b_project([],[event_b_context(none,'RegularGrammar_Ex1',[extends(none,['RegularGrammar']),constants(none,[identifier(none,a),identifier(none,b)]),abstract_constants(none,[]),axioms(none,[partition(rodinpos('RegularGrammar_Ex1',axm1,'__-kccM7VEeOrle-yLgG2VQ'),identifier(none,'Terminals'),[set_extension(none,[identifier(none,a)]),set_extension(none,[identifier(none,b)])]),equal(rodinpos('RegularGrammar_Ex1',axm2,'__-kccc7VEeOrle-yLgG2VQ'),identifier(none,'P'),set_extension(none,[couple(none,[identifier(none,'S'),couple(none,[identifier(none,a),identifier(none,'S')])]),couple(none,[identifier(none,'S'),couple(none,[identifier(none,b),identifier(none,'S')])]),couple(none,[identifier(none,'S'),couple(none,[identifier(none,b),identifier(none,none)])])]))]),theorems(none,[]),sets(none,[])]),event_b_context(none,'RegularGrammar',[extends(none,['Symbols']),constants(none,[identifier(none,'P'),identifier(none,'S'),identifier(none,none)]),abstract_constants(none,[]),axioms(none,[conjunct(rodinpos('RegularGrammar',axm1,'_FXO_sM7VEeOrle-yLgG2VQ'),member(none,identifier(none,none),identifier(none,'NonTerminals')),not_equal(none,identifier(none,none),identifier(none,'S'))),member(rodinpos('RegularGrammar',axm2,'_6OP5EM7UEeOrle-yLgG2VQ'),identifier(none,'S'),identifier(none,'NonTerminals')),member(rodinpos('RegularGrammar',axm3,'_6OP5Ec7UEeOrle-yLgG2VQ'),identifier(none,'P'),relations(none,set_subtraction(none,identifier(none,'NonTerminals'),set_extension(none,[identifier(none,none)])),cartesian_product(none,identifier(none,'Terminals'),identifier(none,'NonTerminals'))))]),theorems(none,[]),sets(none,[])]),event_b_context(none,'Symbols',[extends(none,[]),constants(none,[identifier(none,'NonTerminals'),identifier(none,'Terminals')]),abstract_constants(none,[]),axioms(none,[partition(rodinpos('Symbols',axm1,'_a5ZWEs7UEeOrle-yLgG2VQ'),identifier(none,'Symbols'),[identifier(none,'Terminals'),identifier(none,'NonTerminals')])]),theorems(none,[]),sets(none,[deferred_set(none,'Symbols')])])],[exporter_version(3)],_Error)).
2