1		generated(1484650124476,'Tue Jan 17 11:48:44 CET 2017').
2		project_name('COMPONENT').
3		machine_name('LOCKR1').
4		disprover_po('INITIALISATION/inv5/INV',event_b_context(none,'DisproverContext',[axioms(none,[member(none,identifier(none,'READY'),identifier(none,'State')),member(none,identifier(none,'initiator_enabled\''),bool_set(none)),member(none,identifier(none,'LOCKED'),identifier(none,'State')),member(none,identifier(none,'LockDeadline'),identifier(none,'Deadline')),member(none,identifier(none,'LOCKING'),identifier(none,'State')),member(none,identifier(none,'locked\''),bool_set(none)),member(none,identifier(none,'completer_evaluated\''),bool_set(none)),member(none,identifier(none,'IDLE'),identifier(none,'State')),member(none,identifier(none,'deadline\''),pow_subset(none,cartesian_product(none,identifier(none,'Deadline'),integer_set(none)))),member(none,identifier(none,'state\''),identifier(none,'State')),member(none,identifier(none,'initiator_evaluated\''),bool_set(none)),partition(none,identifier(none,'State'),[set_extension(none,[identifier(none,'IDLE')]),set_extension(none,[identifier(none,'READY')]),set_extension(none,[identifier(none,'LOCKING')]),set_extension(none,[identifier(none,'LOCKED')])]),member(none,identifier(none,'LockDeadline'),identifier(none,'Deadline'))]),constants(none,[identifier(none,'READY'),identifier(none,'initiator_enabled\''),identifier(none,'LOCKED'),identifier(none,'LockDeadline'),identifier(none,'LOCKING'),identifier(none,'locked\''),identifier(none,'completer_evaluated\''),identifier(none,'IDLE'),identifier(none,'deadline\''),identifier(none,'state\''),identifier(none,'initiator_evaluated\'')]),sets(none,[deferred_set(none,'Deadline'),deferred_set(none,'State')])]),member(none,typeof(none,empty_set(none),pow_subset(none,cartesian_product(none,identifier(none,'Deadline'),integer_set(none)))),partial_function(none,identifier(none,'Deadline'),natural_set(none))),[partition(none,identifier(none,'State'),[set_extension(none,[identifier(none,'IDLE')]),set_extension(none,[identifier(none,'READY')]),set_extension(none,[identifier(none,'LOCKING')]),set_extension(none,[identifier(none,'LOCKED')])]),member(none,identifier(none,'LockDeadline'),identifier(none,'Deadline'))],[],true).
5		disprover_po('INITIALISATION/inv6/INV',event_b_context(none,'DisproverContext',[axioms(none,[member(none,identifier(none,'READY'),identifier(none,'State')),member(none,identifier(none,'initiator_enabled\''),bool_set(none)),member(none,identifier(none,'LOCKED'),identifier(none,'State')),member(none,identifier(none,'LockDeadline'),identifier(none,'Deadline')),member(none,identifier(none,'LOCKING'),identifier(none,'State')),member(none,identifier(none,'locked\''),bool_set(none)),member(none,identifier(none,'completer_evaluated\''),bool_set(none)),member(none,identifier(none,'IDLE'),identifier(none,'State')),member(none,identifier(none,'deadline\''),pow_subset(none,cartesian_product(none,identifier(none,'Deadline'),integer_set(none)))),member(none,identifier(none,'state\''),identifier(none,'State')),member(none,identifier(none,'initiator_evaluated\''),bool_set(none)),partition(none,identifier(none,'State'),[set_extension(none,[identifier(none,'IDLE')]),set_extension(none,[identifier(none,'READY')]),set_extension(none,[identifier(none,'LOCKING')]),set_extension(none,[identifier(none,'LOCKED')])]),member(none,identifier(none,'LockDeadline'),identifier(none,'Deadline'))]),constants(none,[identifier(none,'READY'),identifier(none,'initiator_enabled\''),identifier(none,'LOCKED'),identifier(none,'LockDeadline'),identifier(none,'LOCKING'),identifier(none,'locked\''),identifier(none,'completer_evaluated\''),identifier(none,'IDLE'),identifier(none,'deadline\''),identifier(none,'state\''),identifier(none,'initiator_evaluated\'')]),sets(none,[deferred_set(none,'Deadline'),deferred_set(none,'State')])]),implication(none,equal(none,identifier(none,'IDLE'),identifier(none,'LOCKED')),member(none,identifier(none,'LockDeadline'),domain(none,typeof(none,empty_set(none),pow_subset(none,cartesian_product(none,identifier(none,'Deadline'),integer_set(none))))))),[partition(none,identifier(none,'State'),[set_extension(none,[identifier(none,'IDLE')]),set_extension(none,[identifier(none,'READY')]),set_extension(none,[identifier(none,'LOCKING')]),set_extension(none,[identifier(none,'LOCKED')])]),member(none,identifier(none,'LockDeadline'),identifier(none,'Deadline'))],[],true).
6		disprover_po('EnableInitiator/inv6/INV',event_b_context(none,'DisproverContext',[axioms(none,[member(none,identifier(none,'READY'),identifier(none,'State')),member(none,identifier(none,'initiator_enabled\''),bool_set(none)),member(none,identifier(none,'LOCKED'),identifier(none,'State')),member(none,identifier(none,'LockDeadline'),identifier(none,'Deadline')),member(none,identifier(none,initiator_enabled),bool_set(none)),member(none,identifier(none,'LOCKING'),identifier(none,'State')),member(none,identifier(none,'IDLE'),identifier(none,'State')),member(none,identifier(none,initiator_evaluated),bool_set(none)),member(none,identifier(none,state),identifier(none,'State')),member(none,identifier(none,'state\''),identifier(none,'State')),member(none,identifier(none,completer_evaluated),bool_set(none)),member(none,identifier(none,deadline),pow_subset(none,cartesian_product(none,identifier(none,'Deadline'),integer_set(none)))),member(none,identifier(none,locked),bool_set(none)),partition(none,identifier(none,'State'),[set_extension(none,[identifier(none,'IDLE')]),set_extension(none,[identifier(none,'READY')]),set_extension(none,[identifier(none,'LOCKING')]),set_extension(none,[identifier(none,'LOCKED')])]),member(none,identifier(none,'LockDeadline'),identifier(none,'Deadline')),member(none,identifier(none,locked),bool_set(none)),member(none,identifier(none,initiator_enabled),bool_set(none)),member(none,identifier(none,initiator_evaluated),bool_set(none)),member(none,identifier(none,completer_evaluated),bool_set(none)),member(none,identifier(none,state),identifier(none,'State')),member(none,identifier(none,deadline),partial_function(none,identifier(none,'Deadline'),natural_set(none))),implication(none,equal(none,identifier(none,state),identifier(none,'LOCKED')),member(none,identifier(none,'LockDeadline'),domain(none,identifier(none,deadline)))),equal(none,identifier(none,initiator_enabled),boolean_false(none)),equal(none,identifier(none,state),identifier(none,'IDLE'))]),constants(none,[identifier(none,'READY'),identifier(none,'initiator_enabled\''),identifier(none,'LOCKED'),identifier(none,'LockDeadline'),identifier(none,initiator_enabled),identifier(none,'LOCKING'),identifier(none,'IDLE'),identifier(none,initiator_evaluated),identifier(none,state),identifier(none,'state\''),identifier(none,completer_evaluated),identifier(none,deadline),identifier(none,locked)]),sets(none,[deferred_set(none,'Deadline'),deferred_set(none,'State')])]),implication(none,equal(none,identifier(none,'READY'),identifier(none,'LOCKED')),member(none,identifier(none,'LockDeadline'),domain(none,identifier(none,deadline)))),[partition(none,identifier(none,'State'),[set_extension(none,[identifier(none,'IDLE')]),set_extension(none,[identifier(none,'READY')]),set_extension(none,[identifier(none,'LOCKING')]),set_extension(none,[identifier(none,'LOCKED')])]),member(none,identifier(none,'LockDeadline'),identifier(none,'Deadline')),member(none,identifier(none,locked),bool_set(none)),member(none,identifier(none,initiator_enabled),bool_set(none)),member(none,identifier(none,initiator_evaluated),bool_set(none)),member(none,identifier(none,completer_evaluated),bool_set(none)),member(none,identifier(none,state),identifier(none,'State')),member(none,identifier(none,deadline),partial_function(none,identifier(none,'Deadline'),natural_set(none))),implication(none,equal(none,identifier(none,state),identifier(none,'LOCKED')),member(none,identifier(none,'LockDeadline'),domain(none,identifier(none,deadline)))),equal(none,identifier(none,initiator_enabled),boolean_false(none)),equal(none,identifier(none,state),identifier(none,'IDLE'))],[implication(none,equal(none,identifier(none,state),identifier(none,'LOCKED')),member(none,identifier(none,'LockDeadline'),domain(none,identifier(none,deadline)))),equal(none,identifier(none,initiator_enabled),boolean_false(none)),equal(none,identifier(none,state),identifier(none,'IDLE'))],true).
7		disprover_po('InitiateLock/inv5/INV',event_b_context(none,'DisproverContext',[axioms(none,[member(none,identifier(none,'READY'),identifier(none,'State')),member(none,identifier(none,'LOCKED'),identifier(none,'State')),member(none,identifier(none,'LockDeadline'),identifier(none,'Deadline')),member(none,identifier(none,initiator_enabled),bool_set(none)),member(none,identifier(none,'LOCKING'),identifier(none,'State')),member(none,identifier(none,'IDLE'),identifier(none,'State')),member(none,identifier(none,initiator_evaluated),bool_set(none)),member(none,identifier(none,'deadline\''),pow_subset(none,cartesian_product(none,identifier(none,'Deadline'),integer_set(none)))),member(none,identifier(none,state),identifier(none,'State')),member(none,identifier(none,'state\''),identifier(none,'State')),member(none,identifier(none,completer_evaluated),bool_set(none)),member(none,identifier(none,deadline),pow_subset(none,cartesian_product(none,identifier(none,'Deadline'),integer_set(none)))),member(none,identifier(none,locked),bool_set(none)),member(none,identifier(none,'initiator_evaluated\''),bool_set(none)),partition(none,identifier(none,'State'),[set_extension(none,[identifier(none,'IDLE')]),set_extension(none,[identifier(none,'READY')]),set_extension(none,[identifier(none,'LOCKING')]),set_extension(none,[identifier(none,'LOCKED')])]),member(none,identifier(none,'LockDeadline'),identifier(none,'Deadline')),member(none,identifier(none,locked),bool_set(none)),member(none,identifier(none,initiator_enabled),bool_set(none)),member(none,identifier(none,initiator_evaluated),bool_set(none)),member(none,identifier(none,completer_evaluated),bool_set(none)),member(none,identifier(none,state),identifier(none,'State')),member(none,identifier(none,deadline),partial_function(none,identifier(none,'Deadline'),natural_set(none))),implication(none,equal(none,identifier(none,state),identifier(none,'LOCKED')),member(none,identifier(none,'LockDeadline'),domain(none,identifier(none,deadline)))),equal(none,identifier(none,state),identifier(none,'READY')),equal(none,identifier(none,initiator_evaluated),boolean_false(none))]),constants(none,[identifier(none,'READY'),identifier(none,'LOCKED'),identifier(none,'LockDeadline'),identifier(none,initiator_enabled),identifier(none,'LOCKING'),identifier(none,'IDLE'),identifier(none,initiator_evaluated),identifier(none,'deadline\''),identifier(none,state),identifier(none,'state\''),identifier(none,completer_evaluated),identifier(none,deadline),identifier(none,locked),identifier(none,'initiator_evaluated\'')]),sets(none,[deferred_set(none,'Deadline'),deferred_set(none,'State')])]),member(none,overwrite(none,identifier(none,deadline),set_extension(none,[couple(none,[identifier(none,'LockDeadline'),integer(none,2)])])),partial_function(none,identifier(none,'Deadline'),natural_set(none))),[partition(none,identifier(none,'State'),[set_extension(none,[identifier(none,'IDLE')]),set_extension(none,[identifier(none,'READY')]),set_extension(none,[identifier(none,'LOCKING')]),set_extension(none,[identifier(none,'LOCKED')])]),member(none,identifier(none,'LockDeadline'),identifier(none,'Deadline')),member(none,identifier(none,locked),bool_set(none)),member(none,identifier(none,initiator_enabled),bool_set(none)),member(none,identifier(none,initiator_evaluated),bool_set(none)),member(none,identifier(none,completer_evaluated),bool_set(none)),member(none,identifier(none,state),identifier(none,'State')),member(none,identifier(none,deadline),partial_function(none,identifier(none,'Deadline'),natural_set(none))),implication(none,equal(none,identifier(none,state),identifier(none,'LOCKED')),member(none,identifier(none,'LockDeadline'),domain(none,identifier(none,deadline)))),equal(none,identifier(none,state),identifier(none,'READY')),equal(none,identifier(none,initiator_evaluated),boolean_false(none))],[member(none,identifier(none,deadline),partial_function(none,identifier(none,'Deadline'),natural_set(none))),equal(none,identifier(none,state),identifier(none,'READY')),equal(none,identifier(none,initiator_evaluated),boolean_false(none))],true).
8		disprover_po('InitiateLock/inv6/INV',event_b_context(none,'DisproverContext',[axioms(none,[member(none,identifier(none,'READY'),identifier(none,'State')),member(none,identifier(none,'LOCKED'),identifier(none,'State')),member(none,identifier(none,'LockDeadline'),identifier(none,'Deadline')),member(none,identifier(none,initiator_enabled),bool_set(none)),member(none,identifier(none,'LOCKING'),identifier(none,'State')),member(none,identifier(none,'IDLE'),identifier(none,'State')),member(none,identifier(none,initiator_evaluated),bool_set(none)),member(none,identifier(none,'deadline\''),pow_subset(none,cartesian_product(none,identifier(none,'Deadline'),integer_set(none)))),member(none,identifier(none,state),identifier(none,'State')),member(none,identifier(none,'state\''),identifier(none,'State')),member(none,identifier(none,completer_evaluated),bool_set(none)),member(none,identifier(none,deadline),pow_subset(none,cartesian_product(none,identifier(none,'Deadline'),integer_set(none)))),member(none,identifier(none,locked),bool_set(none)),member(none,identifier(none,'initiator_evaluated\''),bool_set(none)),partition(none,identifier(none,'State'),[set_extension(none,[identifier(none,'IDLE')]),set_extension(none,[identifier(none,'READY')]),set_extension(none,[identifier(none,'LOCKING')]),set_extension(none,[identifier(none,'LOCKED')])]),member(none,identifier(none,'LockDeadline'),identifier(none,'Deadline')),member(none,identifier(none,locked),bool_set(none)),member(none,identifier(none,initiator_enabled),bool_set(none)),member(none,identifier(none,initiator_evaluated),bool_set(none)),member(none,identifier(none,completer_evaluated),bool_set(none)),member(none,identifier(none,state),identifier(none,'State')),member(none,identifier(none,deadline),partial_function(none,identifier(none,'Deadline'),natural_set(none))),implication(none,equal(none,identifier(none,state),identifier(none,'LOCKED')),member(none,identifier(none,'LockDeadline'),domain(none,identifier(none,deadline)))),equal(none,identifier(none,state),identifier(none,'READY')),equal(none,identifier(none,initiator_evaluated),boolean_false(none))]),constants(none,[identifier(none,'READY'),identifier(none,'LOCKED'),identifier(none,'LockDeadline'),identifier(none,initiator_enabled),identifier(none,'LOCKING'),identifier(none,'IDLE'),identifier(none,initiator_evaluated),identifier(none,'deadline\''),identifier(none,state),identifier(none,'state\''),identifier(none,completer_evaluated),identifier(none,deadline),identifier(none,locked),identifier(none,'initiator_evaluated\'')]),sets(none,[deferred_set(none,'Deadline'),deferred_set(none,'State')])]),implication(none,equal(none,identifier(none,'LOCKING'),identifier(none,'LOCKED')),member(none,identifier(none,'LockDeadline'),domain(none,overwrite(none,identifier(none,deadline),set_extension(none,[couple(none,[identifier(none,'LockDeadline'),integer(none,2)])]))))),[partition(none,identifier(none,'State'),[set_extension(none,[identifier(none,'IDLE')]),set_extension(none,[identifier(none,'READY')]),set_extension(none,[identifier(none,'LOCKING')]),set_extension(none,[identifier(none,'LOCKED')])]),member(none,identifier(none,'LockDeadline'),identifier(none,'Deadline')),member(none,identifier(none,locked),bool_set(none)),member(none,identifier(none,initiator_enabled),bool_set(none)),member(none,identifier(none,initiator_evaluated),bool_set(none)),member(none,identifier(none,completer_evaluated),bool_set(none)),member(none,identifier(none,state),identifier(none,'State')),member(none,identifier(none,deadline),partial_function(none,identifier(none,'Deadline'),natural_set(none))),implication(none,equal(none,identifier(none,state),identifier(none,'LOCKED')),member(none,identifier(none,'LockDeadline'),domain(none,identifier(none,deadline)))),equal(none,identifier(none,state),identifier(none,'READY')),equal(none,identifier(none,initiator_evaluated),boolean_false(none))],[implication(none,equal(none,identifier(none,state),identifier(none,'LOCKED')),member(none,identifier(none,'LockDeadline'),domain(none,identifier(none,deadline)))),equal(none,identifier(none,state),identifier(none,'READY')),equal(none,identifier(none,initiator_evaluated),boolean_false(none))],true).
9		disprover_po('CompleteLock/grd3/WD',event_b_context(none,'DisproverContext',[axioms(none,[member(none,identifier(none,'READY'),identifier(none,'State')),member(none,identifier(none,'LOCKED'),identifier(none,'State')),member(none,identifier(none,'LockDeadline'),identifier(none,'Deadline')),member(none,identifier(none,initiator_enabled),bool_set(none)),member(none,identifier(none,'LOCKING'),identifier(none,'State')),member(none,identifier(none,'locked\''),bool_set(none)),member(none,identifier(none,'IDLE'),identifier(none,'State')),member(none,identifier(none,initiator_evaluated),bool_set(none)),member(none,identifier(none,state),identifier(none,'State')),member(none,identifier(none,'state\''),identifier(none,'State')),member(none,identifier(none,completer_evaluated),bool_set(none)),member(none,identifier(none,deadline),pow_subset(none,cartesian_product(none,identifier(none,'Deadline'),integer_set(none)))),member(none,identifier(none,locked),bool_set(none)),partition(none,identifier(none,'State'),[set_extension(none,[identifier(none,'IDLE')]),set_extension(none,[identifier(none,'READY')]),set_extension(none,[identifier(none,'LOCKING')]),set_extension(none,[identifier(none,'LOCKED')])]),member(none,identifier(none,'LockDeadline'),identifier(none,'Deadline')),member(none,identifier(none,locked),bool_set(none)),member(none,identifier(none,initiator_enabled),bool_set(none)),member(none,identifier(none,initiator_evaluated),bool_set(none)),member(none,identifier(none,completer_evaluated),bool_set(none)),member(none,identifier(none,state),identifier(none,'State')),member(none,identifier(none,deadline),partial_function(none,identifier(none,'Deadline'),natural_set(none))),implication(none,equal(none,identifier(none,state),identifier(none,'LOCKED')),member(none,identifier(none,'LockDeadline'),domain(none,identifier(none,deadline)))),equal(none,identifier(none,locked),boolean_false(none)),member(none,identifier(none,'LockDeadline'),domain(none,identifier(none,deadline)))]),constants(none,[identifier(none,'READY'),identifier(none,'LOCKED'),identifier(none,'LockDeadline'),identifier(none,initiator_enabled),identifier(none,'LOCKING'),identifier(none,'locked\''),identifier(none,'IDLE'),identifier(none,initiator_evaluated),identifier(none,state),identifier(none,'state\''),identifier(none,completer_evaluated),identifier(none,deadline),identifier(none,locked)]),sets(none,[deferred_set(none,'Deadline'),deferred_set(none,'State')])]),conjunct(none,member(none,identifier(none,'LockDeadline'),domain(none,identifier(none,deadline))),member(none,identifier(none,deadline),partial_function(none,identifier(none,'Deadline'),integer_set(none)))),[partition(none,identifier(none,'State'),[set_extension(none,[identifier(none,'IDLE')]),set_extension(none,[identifier(none,'READY')]),set_extension(none,[identifier(none,'LOCKING')]),set_extension(none,[identifier(none,'LOCKED')])]),member(none,identifier(none,'LockDeadline'),identifier(none,'Deadline')),member(none,identifier(none,locked),bool_set(none)),member(none,identifier(none,initiator_enabled),bool_set(none)),member(none,identifier(none,initiator_evaluated),bool_set(none)),member(none,identifier(none,completer_evaluated),bool_set(none)),member(none,identifier(none,state),identifier(none,'State')),member(none,identifier(none,deadline),partial_function(none,identifier(none,'Deadline'),natural_set(none))),implication(none,equal(none,identifier(none,state),identifier(none,'LOCKED')),member(none,identifier(none,'LockDeadline'),domain(none,identifier(none,deadline)))),equal(none,identifier(none,locked),boolean_false(none)),member(none,identifier(none,'LockDeadline'),domain(none,identifier(none,deadline)))],[equal(none,identifier(none,locked),boolean_false(none)),member(none,identifier(none,'LockDeadline'),domain(none,identifier(none,deadline)))],true).
10		disprover_po('CompleteLock/inv6/INV',event_b_context(none,'DisproverContext',[axioms(none,[member(none,identifier(none,'READY'),identifier(none,'State')),member(none,identifier(none,'LOCKED'),identifier(none,'State')),member(none,identifier(none,'LockDeadline'),identifier(none,'Deadline')),member(none,identifier(none,initiator_enabled),bool_set(none)),member(none,identifier(none,'LOCKING'),identifier(none,'State')),member(none,identifier(none,'locked\''),bool_set(none)),member(none,identifier(none,'IDLE'),identifier(none,'State')),member(none,identifier(none,initiator_evaluated),bool_set(none)),member(none,identifier(none,state),identifier(none,'State')),member(none,identifier(none,'state\''),identifier(none,'State')),member(none,identifier(none,completer_evaluated),bool_set(none)),member(none,identifier(none,deadline),pow_subset(none,cartesian_product(none,identifier(none,'Deadline'),integer_set(none)))),member(none,identifier(none,locked),bool_set(none)),partition(none,identifier(none,'State'),[set_extension(none,[identifier(none,'IDLE')]),set_extension(none,[identifier(none,'READY')]),set_extension(none,[identifier(none,'LOCKING')]),set_extension(none,[identifier(none,'LOCKED')])]),member(none,identifier(none,'LockDeadline'),identifier(none,'Deadline')),member(none,identifier(none,locked),bool_set(none)),member(none,identifier(none,initiator_enabled),bool_set(none)),member(none,identifier(none,initiator_evaluated),bool_set(none)),member(none,identifier(none,completer_evaluated),bool_set(none)),member(none,identifier(none,state),identifier(none,'State')),member(none,identifier(none,deadline),partial_function(none,identifier(none,'Deadline'),natural_set(none))),implication(none,equal(none,identifier(none,state),identifier(none,'LOCKED')),member(none,identifier(none,'LockDeadline'),domain(none,identifier(none,deadline)))),equal(none,identifier(none,locked),boolean_false(none)),member(none,identifier(none,'LockDeadline'),domain(none,identifier(none,deadline))),equal(none,function(none,identifier(none,deadline),[identifier(none,'LockDeadline')]),integer(none,0)),member(none,identifier(none,deadline),partial_function(none,identifier(none,'Deadline'),integer_set(none))),equal(none,identifier(none,completer_evaluated),boolean_false(none)),equal(none,identifier(none,state),identifier(none,'LOCKING'))]),constants(none,[identifier(none,'READY'),identifier(none,'LOCKED'),identifier(none,'LockDeadline'),identifier(none,initiator_enabled),identifier(none,'LOCKING'),identifier(none,'locked\''),identifier(none,'IDLE'),identifier(none,initiator_evaluated),identifier(none,state),identifier(none,'state\''),identifier(none,completer_evaluated),identifier(none,deadline),identifier(none,locked)]),sets(none,[deferred_set(none,'Deadline'),deferred_set(none,'State')])]),implication(none,equal(none,identifier(none,'LOCKED'),identifier(none,'LOCKED')),member(none,identifier(none,'LockDeadline'),domain(none,identifier(none,deadline)))),[partition(none,identifier(none,'State'),[set_extension(none,[identifier(none,'IDLE')]),set_extension(none,[identifier(none,'READY')]),set_extension(none,[identifier(none,'LOCKING')]),set_extension(none,[identifier(none,'LOCKED')])]),member(none,identifier(none,'LockDeadline'),identifier(none,'Deadline')),member(none,identifier(none,locked),bool_set(none)),member(none,identifier(none,initiator_enabled),bool_set(none)),member(none,identifier(none,initiator_evaluated),bool_set(none)),member(none,identifier(none,completer_evaluated),bool_set(none)),member(none,identifier(none,state),identifier(none,'State')),member(none,identifier(none,deadline),partial_function(none,identifier(none,'Deadline'),natural_set(none))),implication(none,equal(none,identifier(none,state),identifier(none,'LOCKED')),member(none,identifier(none,'LockDeadline'),domain(none,identifier(none,deadline)))),equal(none,identifier(none,locked),boolean_false(none)),member(none,identifier(none,'LockDeadline'),domain(none,identifier(none,deadline))),equal(none,function(none,identifier(none,deadline),[identifier(none,'LockDeadline')]),integer(none,0)),member(none,identifier(none,deadline),partial_function(none,identifier(none,'Deadline'),integer_set(none))),equal(none,identifier(none,completer_evaluated),boolean_false(none)),equal(none,identifier(none,state),identifier(none,'LOCKING'))],[implication(none,equal(none,identifier(none,state),identifier(none,'LOCKED')),member(none,identifier(none,'LockDeadline'),domain(none,identifier(none,deadline)))),equal(none,identifier(none,locked),boolean_false(none)),member(none,identifier(none,'LockDeadline'),domain(none,identifier(none,deadline))),equal(none,function(none,identifier(none,deadline),[identifier(none,'LockDeadline')]),integer(none,0)),equal(none,identifier(none,completer_evaluated),boolean_false(none)),equal(none,identifier(none,state),identifier(none,'LOCKING'))],true).
11		disprover_po('Unlock/inv6/INV',event_b_context(none,'DisproverContext',[axioms(none,[member(none,identifier(none,'READY'),identifier(none,'State')),member(none,identifier(none,'LOCKED'),identifier(none,'State')),member(none,identifier(none,'LockDeadline'),identifier(none,'Deadline')),member(none,identifier(none,initiator_enabled),bool_set(none)),member(none,identifier(none,'LOCKING'),identifier(none,'State')),member(none,identifier(none,'locked\''),bool_set(none)),member(none,identifier(none,'completer_evaluated\''),bool_set(none)),member(none,identifier(none,'IDLE'),identifier(none,'State')),member(none,identifier(none,initiator_evaluated),bool_set(none)),member(none,identifier(none,state),identifier(none,'State')),member(none,identifier(none,'state\''),identifier(none,'State')),member(none,identifier(none,completer_evaluated),bool_set(none)),member(none,identifier(none,deadline),pow_subset(none,cartesian_product(none,identifier(none,'Deadline'),integer_set(none)))),member(none,identifier(none,locked),bool_set(none)),partition(none,identifier(none,'State'),[set_extension(none,[identifier(none,'IDLE')]),set_extension(none,[identifier(none,'READY')]),set_extension(none,[identifier(none,'LOCKING')]),set_extension(none,[identifier(none,'LOCKED')])]),member(none,identifier(none,'LockDeadline'),identifier(none,'Deadline')),member(none,identifier(none,locked),bool_set(none)),member(none,identifier(none,initiator_enabled),bool_set(none)),member(none,identifier(none,initiator_evaluated),bool_set(none)),member(none,identifier(none,completer_evaluated),bool_set(none)),member(none,identifier(none,state),identifier(none,'State')),member(none,identifier(none,deadline),partial_function(none,identifier(none,'Deadline'),natural_set(none))),implication(none,equal(none,identifier(none,state),identifier(none,'LOCKED')),member(none,identifier(none,'LockDeadline'),domain(none,identifier(none,deadline)))),equal(none,identifier(none,locked),boolean_true(none)),equal(none,identifier(none,state),identifier(none,'LOCKED'))]),constants(none,[identifier(none,'READY'),identifier(none,'LOCKED'),identifier(none,'LockDeadline'),identifier(none,initiator_enabled),identifier(none,'LOCKING'),identifier(none,'locked\''),identifier(none,'completer_evaluated\''),identifier(none,'IDLE'),identifier(none,initiator_evaluated),identifier(none,state),identifier(none,'state\''),identifier(none,completer_evaluated),identifier(none,deadline),identifier(none,locked)]),sets(none,[deferred_set(none,'Deadline'),deferred_set(none,'State')])]),implication(none,equal(none,identifier(none,'IDLE'),identifier(none,'LOCKED')),member(none,identifier(none,'LockDeadline'),domain(none,identifier(none,deadline)))),[partition(none,identifier(none,'State'),[set_extension(none,[identifier(none,'IDLE')]),set_extension(none,[identifier(none,'READY')]),set_extension(none,[identifier(none,'LOCKING')]),set_extension(none,[identifier(none,'LOCKED')])]),member(none,identifier(none,'LockDeadline'),identifier(none,'Deadline')),member(none,identifier(none,locked),bool_set(none)),member(none,identifier(none,initiator_enabled),bool_set(none)),member(none,identifier(none,initiator_evaluated),bool_set(none)),member(none,identifier(none,completer_evaluated),bool_set(none)),member(none,identifier(none,state),identifier(none,'State')),member(none,identifier(none,deadline),partial_function(none,identifier(none,'Deadline'),natural_set(none))),implication(none,equal(none,identifier(none,state),identifier(none,'LOCKED')),member(none,identifier(none,'LockDeadline'),domain(none,identifier(none,deadline)))),equal(none,identifier(none,locked),boolean_true(none)),equal(none,identifier(none,state),identifier(none,'LOCKED'))],[implication(none,equal(none,identifier(none,state),identifier(none,'LOCKED')),member(none,identifier(none,'LockDeadline'),domain(none,identifier(none,deadline)))),equal(none,identifier(none,locked),boolean_true(none)),equal(none,identifier(none,state),identifier(none,'LOCKED'))],true).
12		disprover_po('Update/inv5/INV',event_b_context(none,'DisproverContext',[axioms(none,[member(none,identifier(none,'READY'),identifier(none,'State')),member(none,identifier(none,'initiator_enabled\''),bool_set(none)),member(none,identifier(none,'LOCKED'),identifier(none,'State')),member(none,identifier(none,'LockDeadline'),identifier(none,'Deadline')),member(none,identifier(none,initiator_enabled),bool_set(none)),member(none,identifier(none,'LOCKING'),identifier(none,'State')),member(none,identifier(none,'completer_evaluated\''),bool_set(none)),member(none,identifier(none,'IDLE'),identifier(none,'State')),member(none,identifier(none,initiator_evaluated),bool_set(none)),member(none,identifier(none,'deadline\''),pow_subset(none,cartesian_product(none,identifier(none,'Deadline'),integer_set(none)))),member(none,identifier(none,state),identifier(none,'State')),member(none,identifier(none,completer_evaluated),bool_set(none)),member(none,identifier(none,deadline),pow_subset(none,cartesian_product(none,identifier(none,'Deadline'),integer_set(none)))),member(none,identifier(none,locked),bool_set(none)),member(none,identifier(none,'initiator_evaluated\''),bool_set(none)),partition(none,identifier(none,'State'),[set_extension(none,[identifier(none,'IDLE')]),set_extension(none,[identifier(none,'READY')]),set_extension(none,[identifier(none,'LOCKING')]),set_extension(none,[identifier(none,'LOCKED')])]),member(none,identifier(none,'LockDeadline'),identifier(none,'Deadline')),member(none,identifier(none,locked),bool_set(none)),member(none,identifier(none,initiator_enabled),bool_set(none)),member(none,identifier(none,initiator_evaluated),bool_set(none)),member(none,identifier(none,completer_evaluated),bool_set(none)),member(none,identifier(none,state),identifier(none,'State')),member(none,identifier(none,deadline),partial_function(none,identifier(none,'Deadline'),natural_set(none))),implication(none,equal(none,identifier(none,state),identifier(none,'LOCKED')),member(none,identifier(none,'LockDeadline'),domain(none,identifier(none,deadline)))),disjunct(none,equal(none,identifier(none,initiator_enabled),boolean_false(none)),equal(none,identifier(none,initiator_evaluated),boolean_true(none))),disjunct(none,not_member(none,integer(none,0),range(none,identifier(none,deadline))),equal(none,identifier(none,completer_evaluated),boolean_true(none))),forall(none,[identifier(none,d)],implication(none,conjunct(none,member(none,identifier(none,d),identifier(none,'Deadline')),member(none,identifier(none,d),domain(none,identifier(none,deadline)))),member(none,identifier(none,deadline),partial_function(none,identifier(none,'Deadline'),integer_set(none)))))]),constants(none,[identifier(none,'READY'),identifier(none,'initiator_enabled\''),identifier(none,'LOCKED'),identifier(none,'LockDeadline'),identifier(none,initiator_enabled),identifier(none,'LOCKING'),identifier(none,'completer_evaluated\''),identifier(none,'IDLE'),identifier(none,initiator_evaluated),identifier(none,'deadline\''),identifier(none,state),identifier(none,completer_evaluated),identifier(none,deadline),identifier(none,locked),identifier(none,'initiator_evaluated\'')]),sets(none,[deferred_set(none,'Deadline'),deferred_set(none,'State')])]),member(none,event_b_comprehension_set(none,[identifier(none,d)],couple(none,[identifier(none,d),minus(none,function(none,identifier(none,deadline),[identifier(none,d)]),integer(none,1))]),conjunct(none,member(none,identifier(none,d),identifier(none,'Deadline')),conjunct(none,member(none,identifier(none,d),domain(none,identifier(none,deadline))),greater(none,function(none,identifier(none,deadline),[identifier(none,d)]),integer(none,0))))),partial_function(none,identifier(none,'Deadline'),natural_set(none))),[partition(none,identifier(none,'State'),[set_extension(none,[identifier(none,'IDLE')]),set_extension(none,[identifier(none,'READY')]),set_extension(none,[identifier(none,'LOCKING')]),set_extension(none,[identifier(none,'LOCKED')])]),member(none,identifier(none,'LockDeadline'),identifier(none,'Deadline')),member(none,identifier(none,locked),bool_set(none)),member(none,identifier(none,initiator_enabled),bool_set(none)),member(none,identifier(none,initiator_evaluated),bool_set(none)),member(none,identifier(none,completer_evaluated),bool_set(none)),member(none,identifier(none,state),identifier(none,'State')),member(none,identifier(none,deadline),partial_function(none,identifier(none,'Deadline'),natural_set(none))),implication(none,equal(none,identifier(none,state),identifier(none,'LOCKED')),member(none,identifier(none,'LockDeadline'),domain(none,identifier(none,deadline)))),disjunct(none,equal(none,identifier(none,initiator_enabled),boolean_false(none)),equal(none,identifier(none,initiator_evaluated),boolean_true(none))),disjunct(none,not_member(none,integer(none,0),range(none,identifier(none,deadline))),equal(none,identifier(none,completer_evaluated),boolean_true(none))),forall(none,[identifier(none,d)],implication(none,conjunct(none,member(none,identifier(none,d),identifier(none,'Deadline')),member(none,identifier(none,d),domain(none,identifier(none,deadline)))),member(none,identifier(none,deadline),partial_function(none,identifier(none,'Deadline'),integer_set(none)))))],[member(none,identifier(none,deadline),partial_function(none,identifier(none,'Deadline'),natural_set(none))),disjunct(none,equal(none,identifier(none,initiator_enabled),boolean_false(none)),equal(none,identifier(none,initiator_evaluated),boolean_true(none))),disjunct(none,not_member(none,integer(none,0),range(none,identifier(none,deadline))),equal(none,identifier(none,completer_evaluated),boolean_true(none)))],true).
13		disprover_po('Update/inv6/INV',event_b_context(none,'DisproverContext',[axioms(none,[member(none,identifier(none,'READY'),identifier(none,'State')),member(none,identifier(none,'initiator_enabled\''),bool_set(none)),member(none,identifier(none,'LOCKED'),identifier(none,'State')),member(none,identifier(none,'LockDeadline'),identifier(none,'Deadline')),member(none,identifier(none,initiator_enabled),bool_set(none)),member(none,identifier(none,'LOCKING'),identifier(none,'State')),member(none,identifier(none,'completer_evaluated\''),bool_set(none)),member(none,identifier(none,'IDLE'),identifier(none,'State')),member(none,identifier(none,initiator_evaluated),bool_set(none)),member(none,identifier(none,'deadline\''),pow_subset(none,cartesian_product(none,identifier(none,'Deadline'),integer_set(none)))),member(none,identifier(none,state),identifier(none,'State')),member(none,identifier(none,completer_evaluated),bool_set(none)),member(none,identifier(none,deadline),pow_subset(none,cartesian_product(none,identifier(none,'Deadline'),integer_set(none)))),member(none,identifier(none,locked),bool_set(none)),member(none,identifier(none,'initiator_evaluated\''),bool_set(none)),partition(none,identifier(none,'State'),[set_extension(none,[identifier(none,'IDLE')]),set_extension(none,[identifier(none,'READY')]),set_extension(none,[identifier(none,'LOCKING')]),set_extension(none,[identifier(none,'LOCKED')])]),member(none,identifier(none,'LockDeadline'),identifier(none,'Deadline')),member(none,identifier(none,locked),bool_set(none)),member(none,identifier(none,initiator_enabled),bool_set(none)),member(none,identifier(none,initiator_evaluated),bool_set(none)),member(none,identifier(none,completer_evaluated),bool_set(none)),member(none,identifier(none,state),identifier(none,'State')),member(none,identifier(none,deadline),partial_function(none,identifier(none,'Deadline'),natural_set(none))),implication(none,equal(none,identifier(none,state),identifier(none,'LOCKED')),member(none,identifier(none,'LockDeadline'),domain(none,identifier(none,deadline)))),disjunct(none,equal(none,identifier(none,initiator_enabled),boolean_false(none)),equal(none,identifier(none,initiator_evaluated),boolean_true(none))),disjunct(none,not_member(none,integer(none,0),range(none,identifier(none,deadline))),equal(none,identifier(none,completer_evaluated),boolean_true(none))),implication(none,equal(none,identifier(none,state),identifier(none,'LOCKED')),forall(none,[identifier(none,d)],implication(none,conjunct(none,member(none,identifier(none,d),identifier(none,'Deadline')),member(none,identifier(none,d),domain(none,identifier(none,deadline)))),member(none,identifier(none,deadline),partial_function(none,identifier(none,'Deadline'),integer_set(none))))))]),constants(none,[identifier(none,'READY'),identifier(none,'initiator_enabled\''),identifier(none,'LOCKED'),identifier(none,'LockDeadline'),identifier(none,initiator_enabled),identifier(none,'LOCKING'),identifier(none,'completer_evaluated\''),identifier(none,'IDLE'),identifier(none,initiator_evaluated),identifier(none,'deadline\''),identifier(none,state),identifier(none,completer_evaluated),identifier(none,deadline),identifier(none,locked),identifier(none,'initiator_evaluated\'')]),sets(none,[deferred_set(none,'Deadline'),deferred_set(none,'State')])]),implication(none,equal(none,identifier(none,state),identifier(none,'LOCKED')),member(none,identifier(none,'LockDeadline'),domain(none,event_b_comprehension_set(none,[identifier(none,d)],couple(none,[identifier(none,d),minus(none,function(none,identifier(none,deadline),[identifier(none,d)]),integer(none,1))]),conjunct(none,member(none,identifier(none,d),identifier(none,'Deadline')),conjunct(none,member(none,identifier(none,d),domain(none,identifier(none,deadline))),greater(none,function(none,identifier(none,deadline),[identifier(none,d)]),integer(none,0)))))))),[partition(none,identifier(none,'State'),[set_extension(none,[identifier(none,'IDLE')]),set_extension(none,[identifier(none,'READY')]),set_extension(none,[identifier(none,'LOCKING')]),set_extension(none,[identifier(none,'LOCKED')])]),member(none,identifier(none,'LockDeadline'),identifier(none,'Deadline')),member(none,identifier(none,locked),bool_set(none)),member(none,identifier(none,initiator_enabled),bool_set(none)),member(none,identifier(none,initiator_evaluated),bool_set(none)),member(none,identifier(none,completer_evaluated),bool_set(none)),member(none,identifier(none,state),identifier(none,'State')),member(none,identifier(none,deadline),partial_function(none,identifier(none,'Deadline'),natural_set(none))),implication(none,equal(none,identifier(none,state),identifier(none,'LOCKED')),member(none,identifier(none,'LockDeadline'),domain(none,identifier(none,deadline)))),disjunct(none,equal(none,identifier(none,initiator_enabled),boolean_false(none)),equal(none,identifier(none,initiator_evaluated),boolean_true(none))),disjunct(none,not_member(none,integer(none,0),range(none,identifier(none,deadline))),equal(none,identifier(none,completer_evaluated),boolean_true(none))),implication(none,equal(none,identifier(none,state),identifier(none,'LOCKED')),forall(none,[identifier(none,d)],implication(none,conjunct(none,member(none,identifier(none,d),identifier(none,'Deadline')),member(none,identifier(none,d),domain(none,identifier(none,deadline)))),member(none,identifier(none,deadline),partial_function(none,identifier(none,'Deadline'),integer_set(none))))))],[implication(none,equal(none,identifier(none,state),identifier(none,'LOCKED')),member(none,identifier(none,'LockDeadline'),domain(none,identifier(none,deadline)))),disjunct(none,equal(none,identifier(none,initiator_enabled),boolean_false(none)),equal(none,identifier(none,initiator_evaluated),boolean_true(none))),disjunct(none,not_member(none,integer(none,0),range(none,identifier(none,deadline))),equal(none,identifier(none,completer_evaluated),boolean_true(none)))],true).
14		disprover_po('Update/act4/WD',event_b_context(none,'DisproverContext',[axioms(none,[member(none,identifier(none,'READY'),identifier(none,'State')),member(none,identifier(none,'initiator_enabled\''),bool_set(none)),member(none,identifier(none,'LOCKED'),identifier(none,'State')),member(none,identifier(none,'LockDeadline'),identifier(none,'Deadline')),member(none,identifier(none,initiator_enabled),bool_set(none)),member(none,identifier(none,'LOCKING'),identifier(none,'State')),member(none,identifier(none,'completer_evaluated\''),bool_set(none)),member(none,identifier(none,'IDLE'),identifier(none,'State')),member(none,identifier(none,initiator_evaluated),bool_set(none)),member(none,identifier(none,'deadline\''),pow_subset(none,cartesian_product(none,identifier(none,'Deadline'),integer_set(none)))),member(none,identifier(none,state),identifier(none,'State')),member(none,identifier(none,completer_evaluated),bool_set(none)),member(none,identifier(none,deadline),pow_subset(none,cartesian_product(none,identifier(none,'Deadline'),integer_set(none)))),member(none,identifier(none,locked),bool_set(none)),member(none,identifier(none,'initiator_evaluated\''),bool_set(none)),partition(none,identifier(none,'State'),[set_extension(none,[identifier(none,'IDLE')]),set_extension(none,[identifier(none,'READY')]),set_extension(none,[identifier(none,'LOCKING')]),set_extension(none,[identifier(none,'LOCKED')])]),member(none,identifier(none,'LockDeadline'),identifier(none,'Deadline')),member(none,identifier(none,locked),bool_set(none)),member(none,identifier(none,initiator_enabled),bool_set(none)),member(none,identifier(none,initiator_evaluated),bool_set(none)),member(none,identifier(none,completer_evaluated),bool_set(none)),member(none,identifier(none,state),identifier(none,'State')),member(none,identifier(none,deadline),partial_function(none,identifier(none,'Deadline'),natural_set(none))),implication(none,equal(none,identifier(none,state),identifier(none,'LOCKED')),member(none,identifier(none,'LockDeadline'),domain(none,identifier(none,deadline)))),disjunct(none,equal(none,identifier(none,initiator_enabled),boolean_false(none)),equal(none,identifier(none,initiator_evaluated),boolean_true(none))),disjunct(none,not_member(none,integer(none,0),range(none,identifier(none,deadline))),equal(none,identifier(none,completer_evaluated),boolean_true(none)))]),constants(none,[identifier(none,'READY'),identifier(none,'initiator_enabled\''),identifier(none,'LOCKED'),identifier(none,'LockDeadline'),identifier(none,initiator_enabled),identifier(none,'LOCKING'),identifier(none,'completer_evaluated\''),identifier(none,'IDLE'),identifier(none,initiator_evaluated),identifier(none,'deadline\''),identifier(none,state),identifier(none,completer_evaluated),identifier(none,deadline),identifier(none,locked),identifier(none,'initiator_evaluated\'')]),sets(none,[deferred_set(none,'Deadline'),deferred_set(none,'State')])]),forall(none,[identifier(none,d)],implication(none,conjunct(none,member(none,identifier(none,d),identifier(none,'Deadline')),member(none,identifier(none,d),domain(none,identifier(none,deadline)))),member(none,identifier(none,deadline),partial_function(none,identifier(none,'Deadline'),integer_set(none))))),[partition(none,identifier(none,'State'),[set_extension(none,[identifier(none,'IDLE')]),set_extension(none,[identifier(none,'READY')]),set_extension(none,[identifier(none,'LOCKING')]),set_extension(none,[identifier(none,'LOCKED')])]),member(none,identifier(none,'LockDeadline'),identifier(none,'Deadline')),member(none,identifier(none,locked),bool_set(none)),member(none,identifier(none,initiator_enabled),bool_set(none)),member(none,identifier(none,initiator_evaluated),bool_set(none)),member(none,identifier(none,completer_evaluated),bool_set(none)),member(none,identifier(none,state),identifier(none,'State')),member(none,identifier(none,deadline),partial_function(none,identifier(none,'Deadline'),natural_set(none))),implication(none,equal(none,identifier(none,state),identifier(none,'LOCKED')),member(none,identifier(none,'LockDeadline'),domain(none,identifier(none,deadline)))),disjunct(none,equal(none,identifier(none,initiator_enabled),boolean_false(none)),equal(none,identifier(none,initiator_evaluated),boolean_true(none))),disjunct(none,not_member(none,integer(none,0),range(none,identifier(none,deadline))),equal(none,identifier(none,completer_evaluated),boolean_true(none)))],[disjunct(none,equal(none,identifier(none,initiator_enabled),boolean_false(none)),equal(none,identifier(none,initiator_evaluated),boolean_true(none))),disjunct(none,not_member(none,integer(none,0),range(none,identifier(none,deadline))),equal(none,identifier(none,completer_evaluated),boolean_true(none)))],true).
15