1		generated(1686141020706,'Wed Jun 07 14:30:20 CEST 2023').
2		project_name('Bridge').
3		machine_name(m0_island_bridge).
4		disprover_po('DLF/THM',event_b_context(none,'DisproverContext',[axioms(none,[member(none,identifier(none,red),identifier(none,'LIGHT')),member(none,identifier(none,green),identifier(none,'LIGHT')),member(none,identifier(none,d),integer_set(none)),member(none,identifier(none,n),integer_set(none)),conjunct(none,[member(none,identifier(none,d),natural1_set(none)),equal(none,identifier(none,d),integer(none,3))]),equal(none,identifier(none,'LIGHT'),set_extension(none,[identifier(none,green),identifier(none,red)])),not_equal(none,identifier(none,green),identifier(none,red)),member(none,identifier(none,n),natural_set(none)),less_equal(none,identifier(none,n),identifier(none,d))]),constants(none,[identifier(none,red),identifier(none,green),identifier(none,d),identifier(none,n)]),sets(none,[deferred_set(none,'LIGHT')])]),disjunct(none,less(none,identifier(none,n),identifier(none,d)),greater(none,identifier(none,n),integer(none,0))),[conjunct(none,[member(none,identifier(none,d),natural1_set(none)),equal(none,identifier(none,d),integer(none,3))]),equal(none,identifier(none,'LIGHT'),set_extension(none,[identifier(none,green),identifier(none,red)])),not_equal(none,identifier(none,green),identifier(none,red)),member(none,identifier(none,n),natural_set(none)),less_equal(none,identifier(none,n),identifier(none,d))],[member(none,identifier(none,n),natural_set(none)),less_equal(none,identifier(none,n),identifier(none,d))],true).
5		disprover_po('INITIALISATION/inv1/INV',event_b_context(none,'DisproverContext',[axioms(none,[member(none,identifier(none,red),identifier(none,'LIGHT')),member(none,identifier(none,'n\''),integer_set(none)),member(none,identifier(none,green),identifier(none,'LIGHT')),member(none,identifier(none,d),integer_set(none)),conjunct(none,[member(none,identifier(none,d),natural1_set(none)),equal(none,identifier(none,d),integer(none,3))]),equal(none,identifier(none,'LIGHT'),set_extension(none,[identifier(none,green),identifier(none,red)])),not_equal(none,identifier(none,green),identifier(none,red))]),constants(none,[identifier(none,red),identifier(none,'n\''),identifier(none,green),identifier(none,d)]),sets(none,[deferred_set(none,'LIGHT')])]),member(none,integer(none,0),natural_set(none)),[conjunct(none,[member(none,identifier(none,d),natural1_set(none)),equal(none,identifier(none,d),integer(none,3))]),equal(none,identifier(none,'LIGHT'),set_extension(none,[identifier(none,green),identifier(none,red)])),not_equal(none,identifier(none,green),identifier(none,red))],[],true).
6		disprover_po('INITIALISATION/inv2/INV',event_b_context(none,'DisproverContext',[axioms(none,[member(none,identifier(none,red),identifier(none,'LIGHT')),member(none,identifier(none,'n\''),integer_set(none)),member(none,identifier(none,green),identifier(none,'LIGHT')),member(none,identifier(none,d),integer_set(none)),conjunct(none,[member(none,identifier(none,d),natural1_set(none)),equal(none,identifier(none,d),integer(none,3))]),equal(none,identifier(none,'LIGHT'),set_extension(none,[identifier(none,green),identifier(none,red)])),not_equal(none,identifier(none,green),identifier(none,red))]),constants(none,[identifier(none,red),identifier(none,'n\''),identifier(none,green),identifier(none,d)]),sets(none,[deferred_set(none,'LIGHT')])]),less_equal(none,integer(none,0),identifier(none,d)),[conjunct(none,[member(none,identifier(none,d),natural1_set(none)),equal(none,identifier(none,d),integer(none,3))]),equal(none,identifier(none,'LIGHT'),set_extension(none,[identifier(none,green),identifier(none,red)])),not_equal(none,identifier(none,green),identifier(none,red))],[],true).
7		disprover_po('ML_out/inv1/INV',event_b_context(none,'DisproverContext',[axioms(none,[member(none,identifier(none,red),identifier(none,'LIGHT')),member(none,identifier(none,green),identifier(none,'LIGHT')),member(none,identifier(none,d),integer_set(none)),member(none,identifier(none,'n\''),integer_set(none)),member(none,identifier(none,n),integer_set(none)),conjunct(none,[member(none,identifier(none,d),natural1_set(none)),equal(none,identifier(none,d),integer(none,3))]),equal(none,identifier(none,'LIGHT'),set_extension(none,[identifier(none,green),identifier(none,red)])),not_equal(none,identifier(none,green),identifier(none,red)),member(none,identifier(none,n),natural_set(none)),less_equal(none,identifier(none,n),identifier(none,d)),disjunct(none,less(none,identifier(none,n),identifier(none,d)),greater(none,identifier(none,n),integer(none,0))),less(none,identifier(none,n),identifier(none,d))]),constants(none,[identifier(none,red),identifier(none,green),identifier(none,d),identifier(none,'n\''),identifier(none,n)]),sets(none,[deferred_set(none,'LIGHT')])]),member(none,add(none,identifier(none,n),integer(none,1)),natural_set(none)),[conjunct(none,[member(none,identifier(none,d),natural1_set(none)),equal(none,identifier(none,d),integer(none,3))]),equal(none,identifier(none,'LIGHT'),set_extension(none,[identifier(none,green),identifier(none,red)])),not_equal(none,identifier(none,green),identifier(none,red)),member(none,identifier(none,n),natural_set(none)),less_equal(none,identifier(none,n),identifier(none,d)),disjunct(none,less(none,identifier(none,n),identifier(none,d)),greater(none,identifier(none,n),integer(none,0))),less(none,identifier(none,n),identifier(none,d))],[member(none,identifier(none,n),natural_set(none)),less(none,identifier(none,n),identifier(none,d))],true).
8		disprover_po('ML_out/inv2/INV',event_b_context(none,'DisproverContext',[axioms(none,[member(none,identifier(none,red),identifier(none,'LIGHT')),member(none,identifier(none,green),identifier(none,'LIGHT')),member(none,identifier(none,d),integer_set(none)),member(none,identifier(none,'n\''),integer_set(none)),member(none,identifier(none,n),integer_set(none)),conjunct(none,[member(none,identifier(none,d),natural1_set(none)),equal(none,identifier(none,d),integer(none,3))]),equal(none,identifier(none,'LIGHT'),set_extension(none,[identifier(none,green),identifier(none,red)])),not_equal(none,identifier(none,green),identifier(none,red)),member(none,identifier(none,n),natural_set(none)),less_equal(none,identifier(none,n),identifier(none,d)),disjunct(none,less(none,identifier(none,n),identifier(none,d)),greater(none,identifier(none,n),integer(none,0))),less(none,identifier(none,n),identifier(none,d))]),constants(none,[identifier(none,red),identifier(none,green),identifier(none,d),identifier(none,'n\''),identifier(none,n)]),sets(none,[deferred_set(none,'LIGHT')])]),less_equal(none,add(none,identifier(none,n),integer(none,1)),identifier(none,d)),[conjunct(none,[member(none,identifier(none,d),natural1_set(none)),equal(none,identifier(none,d),integer(none,3))]),equal(none,identifier(none,'LIGHT'),set_extension(none,[identifier(none,green),identifier(none,red)])),not_equal(none,identifier(none,green),identifier(none,red)),member(none,identifier(none,n),natural_set(none)),less_equal(none,identifier(none,n),identifier(none,d)),disjunct(none,less(none,identifier(none,n),identifier(none,d)),greater(none,identifier(none,n),integer(none,0))),less(none,identifier(none,n),identifier(none,d))],[less_equal(none,identifier(none,n),identifier(none,d)),less(none,identifier(none,n),identifier(none,d))],true).
9		disprover_po('ML_in/inv1/INV',event_b_context(none,'DisproverContext',[axioms(none,[member(none,identifier(none,red),identifier(none,'LIGHT')),member(none,identifier(none,green),identifier(none,'LIGHT')),member(none,identifier(none,d),integer_set(none)),member(none,identifier(none,'n\''),integer_set(none)),member(none,identifier(none,n),integer_set(none)),conjunct(none,[member(none,identifier(none,d),natural1_set(none)),equal(none,identifier(none,d),integer(none,3))]),equal(none,identifier(none,'LIGHT'),set_extension(none,[identifier(none,green),identifier(none,red)])),not_equal(none,identifier(none,green),identifier(none,red)),member(none,identifier(none,n),natural_set(none)),less_equal(none,identifier(none,n),identifier(none,d)),disjunct(none,less(none,identifier(none,n),identifier(none,d)),greater(none,identifier(none,n),integer(none,0))),greater(none,identifier(none,n),integer(none,0))]),constants(none,[identifier(none,red),identifier(none,green),identifier(none,d),identifier(none,'n\''),identifier(none,n)]),sets(none,[deferred_set(none,'LIGHT')])]),member(none,minus(none,identifier(none,n),integer(none,1)),natural_set(none)),[conjunct(none,[member(none,identifier(none,d),natural1_set(none)),equal(none,identifier(none,d),integer(none,3))]),equal(none,identifier(none,'LIGHT'),set_extension(none,[identifier(none,green),identifier(none,red)])),not_equal(none,identifier(none,green),identifier(none,red)),member(none,identifier(none,n),natural_set(none)),less_equal(none,identifier(none,n),identifier(none,d)),disjunct(none,less(none,identifier(none,n),identifier(none,d)),greater(none,identifier(none,n),integer(none,0))),greater(none,identifier(none,n),integer(none,0))],[member(none,identifier(none,n),natural_set(none)),greater(none,identifier(none,n),integer(none,0))],true).
10		disprover_po('ML_in/inv2/INV',event_b_context(none,'DisproverContext',[axioms(none,[member(none,identifier(none,red),identifier(none,'LIGHT')),member(none,identifier(none,green),identifier(none,'LIGHT')),member(none,identifier(none,d),integer_set(none)),member(none,identifier(none,'n\''),integer_set(none)),member(none,identifier(none,n),integer_set(none)),conjunct(none,[member(none,identifier(none,d),natural1_set(none)),equal(none,identifier(none,d),integer(none,3))]),equal(none,identifier(none,'LIGHT'),set_extension(none,[identifier(none,green),identifier(none,red)])),not_equal(none,identifier(none,green),identifier(none,red)),member(none,identifier(none,n),natural_set(none)),less_equal(none,identifier(none,n),identifier(none,d)),disjunct(none,less(none,identifier(none,n),identifier(none,d)),greater(none,identifier(none,n),integer(none,0))),greater(none,identifier(none,n),integer(none,0))]),constants(none,[identifier(none,red),identifier(none,green),identifier(none,d),identifier(none,'n\''),identifier(none,n)]),sets(none,[deferred_set(none,'LIGHT')])]),less_equal(none,minus(none,identifier(none,n),integer(none,1)),identifier(none,d)),[conjunct(none,[member(none,identifier(none,d),natural1_set(none)),equal(none,identifier(none,d),integer(none,3))]),equal(none,identifier(none,'LIGHT'),set_extension(none,[identifier(none,green),identifier(none,red)])),not_equal(none,identifier(none,green),identifier(none,red)),member(none,identifier(none,n),natural_set(none)),less_equal(none,identifier(none,n),identifier(none,d)),disjunct(none,less(none,identifier(none,n),identifier(none,d)),greater(none,identifier(none,n),integer(none,0))),greater(none,identifier(none,n),integer(none,0))],[less_equal(none,identifier(none,n),identifier(none,d)),greater(none,identifier(none,n),integer(none,0))],true).
11