1		package(load_event_b_project([event_b_model(none,
2		'Sieve',
3		[sees(none,
4		['SieveContext']),
5		variables(none,
6		[identifier(none,
7		cur),
8		identifier(none,
9		numbers)]),
10		invariant(none,
11		[subset(none,
12		identifier(none,
13		numbers),
14		natural_set(none)),
15		member(none,
16		identifier(none,
17		cur),
18		natural1_set(none))]),
19		theorems(none,
20		[]),
21		events(none,
22		[event(none,
23		'INITIALISATION',
24		[],
25		[],
26		[],
27		[assign(none,
28		[identifier(none,
29		numbers)],
30		[interval(none,
31		integer(none,
32		2),
33		identifier(none,
34		mx))]),
35		assign(none,
36		[identifier(none,
37		cur)],
38		[integer(none,
39		2)])],
40		[]),
41		event(none,
42		treat_prime,
43		[],
44		[],
45		[member(none,
46		identifier(none,
47		cur),
48		identifier(none,
49		numbers)),
50		less_equal(none,
51		multiplication(none,
52		identifier(none,
53		cur),
54		identifier(none,
55		cur)),
56		identifier(none,
57		mx))],
58		[assign(none,
59		[identifier(none,
60		cur)],
61		[add(none,
62		identifier(none,
63		cur),
64		integer(none,
65		1))]),
66		assign(none,
67		[identifier(none,
68		numbers)],
69		[set_subtraction(none,
70		identifier(none,
71		numbers),
72		range(none,
73		event_b_comprehension_set(none,
74		[identifier(none,
75		n)],
76		couple(none,
77		[identifier(none,
78		n),
79		multiplication(none,
80		identifier(none,
81		n),
82		identifier(none,
83		cur))]),
84		member(none,
85		identifier(none,
86		n),
87		interval(none,
88		integer(none,
89		2),
90		div(none,
91		identifier(none,
92		mx),
93		identifier(none,
94		cur)))))))])],
95		[]),
96		event(none,
97		treat_composite,
98		[],
99		[],
100		[less_equal(none,
101		multiplication(none,
102		identifier(none,
103		cur),
104		identifier(none,
105		cur)),
106		identifier(none,
107		mx)),
108		not_member(none,
109		identifier(none,
110		cur),
111		identifier(none,
112		numbers))],
113		[assign(none,
114		[identifier(none,
115		cur)],
116		[add(none,
117		identifier(none,
118		cur),
119		integer(none,
120		1))])],
121		[]),
122		event(none,
123		finished,
124		[],
125		[identifier(none,
126		npr)],
127		[greater(none,
128		multiplication(none,
129		identifier(none,
130		cur),
131		identifier(none,
132		cur)),
133		identifier(none,
134		mx)),
135		equal(none,
136		identifier(none,
137		npr),
138		card(none,
139		identifier(none,
140		numbers)))],
141		[],
142		[])])])],
143		[event_b_context(none,
144		'SieveContext',
145		[extends(none,
146		[]),
147		constants(none,
148		[identifier(none,
149		mx)]),
150		axioms(none,
151		[equal(none,
152		identifier(none,
153		mx),
154		integer(none,
155		1000))]),
156		theorems(none,
157		[]),
158		sets(none,
159		[])])],
160		_Error)).